It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not only an encoding. The question is, what would be the reference for this system?


2 Answers 2


The treatment of pairs given by encoding, such as that in Proofs and Types, isn't what you usually want since they aren't "surjective pairs", i.e., there is no eta rule. Let's call surjective pairs, products.

An extension of system F with products and unit is given in: Di Cosmo, 1995, Isomorphisms of types: from lambda-calculus to information retrieval and language design, Birkhauser: Basel.


You can add arbitrary (positive) inductive types to system F, and show that the system with appropriate eliminators is SN. This is treated in Mendler's thesis here.

  • $\begingroup$ This is also treated, albeit in somewhat sketchy detail, in sections 11.4 and 11.5 of Proofs and Types. $\endgroup$ Jun 11, 2011 at 8:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.