Examples of Independence in the Simple Type Theory in Abella



This webpage contains some supporting material for the paper:

A Proof-theoretic Characterization of Independence in Type Theory” by Yuting Wang and Kaustuv Chaudhuri

You may browse the following development on-line. To run them yourself, you will need Abella in the master branch containing the most recent bug fixes, which is available from the Abella github web-page.

Independence between Types and Terms in Simply Typed Lambda Calculus

Additional Examples of Independence


Additional examples showing the differences between independence and subordination.

Last updated: