λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file proves type safety.

References

• A. Chargueraud, The Locally Nameless Representation
• See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which this is adapted

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.preservation {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {t : Term Var} {Γ : Env Var} {τ : Ty Var} {t' : Term Var} (der : Typing Γ t τ) (step : Term.rs.Red t t') : Typing Γ t' τ

Any reduction step preserves typing.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.progress {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {t : Term Var} {τ : Ty Var} (der : Typing [] t τ) : t.Value ∨ ∃ (t' : Term Var), Term.rs.Red t t'

Any typable term either has a reduction step or is a value.