λ-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 LambdaCalculus.LocallyNameless.Stlc.PreservesTyping {Var : Type u} (R : Untyped.Term Var → Untyped.Term Var → Prop) (Base : Type v) : Prop

Equations

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

theorem LambdaCalculus.LocallyNameless.Stlc.redex_preservesTyping {Var : Type u} {Base : Type v} {R : Untyped.Term Var → Untyped.Term Var → Prop} : PreservesTyping R Base → PreservesTyping (Relation.ReflTransGen R) Base

If a reduction preserves types, so does its reflexive transitive closure.

theorem LambdaCalculus.LocallyNameless.Stlc.confluence_preservesTyping {Var : Type u} {Base : Type v} {R : Untyped.Term Var → Untyped.Term Var → Prop} {Γ : Context Var (Ty Base)} {a b c : Untyped.Term Var} {τ : Ty Base} (con : Confluence R) (p : PreservesTyping R Base) (der : Typing Γ a τ) (ab : Relation.ReflTransGen R a b) (ac : Relation.ReflTransGen R a c) : ∃ (d : Untyped.Term Var), Relation.ReflTransGen R b d ∧ Relation.ReflTransGen R c d ∧ Typing Γ d τ

Confluence preserves type preservation.

theorem LambdaCalculus.LocallyNameless.Stlc.FullBeta.preservation {Var : Type u} {Base : Type v} [HasFresh Var] [DecidableEq Var] {Γ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} {t' : Untyped.Term Var} (der : Typing Γ t τ) (step : t ⭢βᶠ t') : Typing Γ t' τ

Typing preservation for full beta reduction.

theorem 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 ⭢βᶠ t'

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