The five typing rules of pure System F

7 fully proved

System F

InductiveExtrinsic typing of pure System F terms#✓fully proved

Extrinsic typing of scoped pure System F terms.

inductive Typing : {n m : Nat} → Ctx n m → Tm n m → Ty n → Prop where
  | var {n m : Nat} {Γ : Ctx n m} (i : Fin m) :
      Typing Γ (.var i) (Γ i)
  | lam {n m : Nat} {Γ : Ctx n m} {A B : Ty n} {b : Tm n (m + 1)} :
      Typing (Fin.cases A Γ) b B → Typing Γ (.lam A b) (.arr A B)
  | app {n m : Nat} {Γ : Ctx n m} {A B : Ty n} {f a : Tm n m} :
      Typing Γ f (.arr A B) → Typing Γ a A → Typing Γ (.app f a) B
  | tabs {n m : Nat} {Γ : Ctx n m} {b : Tm (n + 1) m} {C : Ty (n + 1)} :
      Typing (fun i => (Γ i).rename Fin.succ) b C →
      Typing Γ (.tabs b) (.all C)
  | tapp {n m : Nat} {Γ : Ctx n m} {f : Tm n m} {A : Ty n}
      {C : Ty (n + 1)} :
      Typing Γ f (.all C) → Typing Γ (.tapp f A) (C.instantiate A)

Uses 5 · Used by 20

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Scoped types of pure System F · Instantiating the newest type binder of a type · Type-variable renaming in System F types

Used byCanonical embedding preserves System F typing · Term translation preserves System F typing · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Type preservation along evaluation sequences · Progress for well-typed terms without free term variables · Type safety for closed well-typed terms · No closed System F term inhabits \(\forall X, X\) · Fundamental theorem of relational parametricity for System F · Closed typed System F terms are related to themselves · Typing of the polymorphic identity · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations · Instantiating a term binder preserves typing · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing

Typing

TheoremType substitution preserves typing#✓fully proved

Type substitution preserves typing, including every context type.

theorem tySubst {k : Nat} (h : Typing Γ t A) (σ : Fin n → Ty k) :
    Typing (fun i => (Γ i).subst σ) (t.tySubst σ) (A.subst σ)

Uses 11 · Used by 2

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Type substitution in System F terms · Scoped types of pure System F · Simultaneous type substitution in System F types · Extrinsic typing of pure System F terms

Proof usesInstantiating the newest type binder of a type · Lifting a type substitution under a type binder · Type-variable renaming in System F types · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening

Used byInstantiating a type binder preserves typing · Type renaming preserves typing

TheoremType renaming preserves typing#✓fully proved

Type renaming preserves typing without adding term variables.

theorem tyRename {k : Nat} (h : Typing Γ t A) (ρ : Fin n → Fin k) :
    Typing (fun i => (Γ i).rename ρ) (t.tyRename ρ) (A.rename ρ)

Uses 10 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Type-variable renaming in System F terms · Scoped types of pure System F · Type-variable renaming in System F types · Extrinsic typing of pure System F terms

Proof usesType substitution in System F terms · Simultaneous type substitution in System F types · Variable-valued substitution is a type renaming · Type substitution preserves typing

Used byTerm substitution preserves typing

TheoremTerm renaming preserves typing#✓fully proved

A context-respecting term renaming preserves the type.

theorem rename {k : Nat} {Δ : Ctx n k} (h : Typing Γ t A)
    (ρ : Fin m → Fin k) (hρ : ∀ i, Δ (ρ i) = Γ i) :
    Typing Δ (t.rename ρ) A

Uses 8 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Term-variable renaming in System F terms · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesInstantiating the newest type binder of a type · Type-variable renaming in System F types · Lifting a scoped renaming under a binder

Used byTerm substitution preserves typing

TheoremTerm substitution preserves typing#✓fully proved

Correctly typed simultaneous term substitution preserves typing.

theorem subst {k : Nat} {Δ : Ctx n k} (h : Typing Γ t A)
    (σ : Fin m → Tm n k) (hσ : ∀ i, Typing Δ (σ i) (Γ i)) :
    Typing Δ (t.subst σ) A

Uses 11 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Simultaneous term substitution in System F terms · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesLifting a term substitution under a term lambda · Type-variable renaming in System F terms · Instantiating the newest type binder of a type · Type-variable renaming in System F types · Term renaming preserves typing · Type renaming preserves typing

Used byInstantiating a term binder preserves typing

TheoremInstantiating a term binder preserves typing#✓fully proved

Discharging a term binder preserves the body type.

theorem instantiate {B : Ty n} {b : Tm n (m + 1)} {a : Tm n m}
    (hb : Typing (Fin.cases A Γ) b B) (ha : Typing Γ a A) :
    Typing Γ (b.instantiate a) B

Uses 6 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Instantiating the newest term binder of a term · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesTerm substitution preserves typing

Used byType preservation for a call-by-value step

TheoremInstantiating a type binder preserves typing#✓fully proved

Type binder discharge substitutes the type and restores the context.

theorem tyInstantiate {b : Tm (n + 1) m} {C : Ty (n + 1)}
    (hb : Typing (fun i => (Γ i).rename Fin.succ) b C) (A : Ty n) :
    Typing Γ (b.tySubst (Fin.cases A Ty.var)) (C.instantiate A)

Uses 10 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Type substitution in System F terms · Scoped types of pure System F · Instantiating the newest type binder of a type · Type-variable renaming in System F types · Extrinsic typing of pure System F terms

Proof usesInstantiating a weakened type restores it · Simultaneous type substitution in System F types · Type substitution preserves typing

Used byType preservation for a call-by-value step

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.