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?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
0
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.
$\begingroup$
$\endgroup$
1
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