Summer school 2008:Exercises 2

From The Twelf Project
Jump to: navigation, search
Summer school 2008

System F (solution)

  1. Give an LF encoding of System F (the polymorphic lambda-calculus). Use PFPL Chapter 25 as the on-paper definition.
  2. Prove adequacy. You may want to follow the adequacy proof in MMLF, section 3.2, page 21.

System F, Intrinsic Encoding

  1. Use an intrinsic encoding to represent only the well-typed System F terms.
  2. What can you say about adequacy for this encoding?

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 MMLF.

Summer school 2008