λ-calculus

Type safety of the simply typed λ-calculus, with a locally nameless representation of syntax. Theorems in this file are namespaced by their respective reductions.

References

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

def Cslib.LambdaCalculus.LocallyNameless.Stlc.PreservesTyping {Var : Type u} (R : Untyped.Term Var → Untyped.Term Var → Prop) (Base : Type v) : Prop

A relation on terms preserves typing if all related terms have the same type.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.FullBeta.preservation {Var : Type u} {Base : Type v} [HasFresh Var] [DecidableEq Var] : PreservesTyping (fun (x1 x2 : Untyped.Term Var) => x1.FullBeta x2) Base

Typing preservation for full beta reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.FullBeta.progress {Var : Type u} {Base : Type v} {t : Untyped.Term Var} {τ : Ty Base} (ht : Typing [] t τ) : t.Value ∨ ∃ (t' : Untyped.Term Var), t.FullBeta t'

A typed term either full beta reduces or is a value.