Documentation out of dateLearn more
Summer school 2008:Exercises 2
- Give an LF encoding of System F (the polymorphic lambda-calculus). Use [http://www.cs.cmu.edu/~rwh/plbook/book.pdf PFPL Chapter 25 as the on-paper definition].
- Prove adequacy. You may want to follow the adequacy proof in [http://www.cs.cmu.edu/~drl/pubs/hl07mechanizing/hl07mechanizing.pdf MMLF], section 3.2, page 21.
System F, Intrinsic Encoding
Section titled “System F, Intrinsic Encoding”- Use an intrinsic encoding to represent only the well-typed System F terms.
- What can you say about adequacy for this encoding?
Hereditary substitution
Section titled “Hereditary substitution”Hereditary substitution is used in the definition of LF to compute the canonical result of substituting one canonical term into another. Read and understand the rules for hereditary substitution in [http://www.cs.cmu.edu/~drl/pubs/hl07mechanizing/hl07mechanizing.pdf MMLF].