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

• stlc contains strengthening lemmas that show types in simply typed lambda calculus (STLC) do not depend on terms a) in an empty context , and b) in a context containing terms .

Additional Examples of Independence

Additional examples showing the differences between independence and subordination.

• str. Given (p => q) => r => r, p is subordinate to r. However, r is independent of p.
• str1. By adding a clause q => r that introduces the dependence between q and r, p is still subordinate to r. However, r is no longer independent of p.

---

Last updated: Thu Feb 26 16:03:00 CST 2015