Call-by-value safety for pure System F

InductiveValue forms of pure System F#✓fully proved

The two value forms of pure System F.

inductive Value : {n m : Nat} → Tm n m → Prop where
  | lam {n m : Nat} {A : Ty n} {b : Tm n (m + 1)} : Value (.lam A b)
  | tabs {n m : Nat} {b : Tm (n + 1) m} : Value (.tabs b)

Uses 2 · Used by 9

Statement usesScoped terms of pure System F · Scoped types of pure System F

Used byTerm translation simulates each weak call-by-value step · Term translation preserves weak call-by-value values · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Progress for well-typed terms without free term variables · Type safety for closed well-typed terms · One-step call-by-value evaluation · Erasure of a System F evaluation step is a beta conversion

InductiveOne-step call-by-value evaluation#✓fully proved

One step of weak, left-to-right call-by-value evaluation.

inductive Step : {n m : Nat} → Tm n m → Tm n m → Prop where
  | appFun {n m : Nat} {f f' a : Tm n m} :
      Step f f' → Step (.app f a) (.app f' a)
  | appArg {n m : Nat} {f a a' : Tm n m} :
      Value f → Step a a' → Step (.app f a) (.app f a')
  | beta {n m : Nat} {A : Ty n} {b : Tm n (m + 1)} {a : Tm n m} :
      Value a → Step (.app (.lam A b) a) (b.instantiate a)
  | tappFun {n m : Nat} {f f' : Tm n m} {A : Ty n} :
      Step f f' → Step (.tapp f A) (.tapp f' A)
  | tyBeta {n m : Nat} {b : Tm (n + 1) m} {A : Ty n} :
      Step (.tapp (.tabs b) A) (b.tySubst (Fin.cases A Ty.var))

Uses 5 · Used by 10

Statement usesScoped terms of pure System F · Instantiating the newest term binder of a term · Type substitution in System F terms · Scoped types of pure System F · Value forms of pure System F

Used byCanonical embedding preserves single evaluation steps · Canonical embedding preserves multistep evaluation · Term translation simulates each weak call-by-value step · 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 · Multi-step call-by-value evaluation · Erasure of a System F evaluation step is a beta conversion · Erasure of multistep System F evaluation is a beta conversion

AbbreviationMulti-step call-by-value evaluation#✓fully proved

Zero or more call-by-value evaluation steps.

abbrev Steps {n m : Nat} : Tm n m → Tm n m → Prop :=
  Relation.ReflTransGen Step

Uses 2 · Used by 4

Statement usesOne-step call-by-value evaluation · Scoped terms of pure System F

Used byCanonical embedding preserves multistep evaluation · Type preservation along evaluation sequences · Type safety for closed well-typed terms · Erasure of multistep System F evaluation is a beta conversion

TheoremType preservation for a call-by-value step#✓fully proved

A call-by-value step preserves the exact type in arbitrary open contexts.

theorem preservation (ht : Typing Γ t A) (hs : Step t t') :
    Typing Γ t' A

Uses 12 · Used by 1

Statement usesTerm variable contexts of System F · One-step call-by-value evaluation · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesInstantiating the newest term binder of a term · Type substitution in System F terms · Instantiating the newest type binder of a type · Type-variable renaming in System F types · Instantiating a term binder preserves typing · Instantiating a type binder preserves typing · Value forms of pure System F

Used byType preservation along evaluation sequences

TheoremCanonical forms of function-typed values#✓fully proved

A function-typed value is a term lambda with the declared argument type.

theorem Typing.canonical_lam {B : Ty n} (ht : Typing Γ t (.arr A B))
    (hv : Value t) : ∃ b : Tm n (m + 1), t = .lam A b

Uses 7 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms · Value forms of pure System F

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

Used byProgress for well-typed terms without free term variables

TheoremCanonical forms of universally typed values#✓fully proved

A universally typed value is a type lambda.

theorem Typing.canonical_tabs {C : Ty (n + 1)}
    (ht : Typing Γ t (.all C)) (hv : Value t) :
    ∃ b : Tm (n + 1) m, t = .tabs b

Uses 7 · Used by 1

Statement usesTerm variable contexts of System F · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms · Value forms of pure System F

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

Used byProgress for well-typed terms without free term variables

TheoremProgress for well-typed terms without free term variables#✓fully proved

A well-typed term with no free term variables is a value or can step.

theorem progress {Γ : Ctx n 0} {t : Tm n 0} (ht : Typing Γ t A) :
    Value t ∨ ∃ t', Step t t'

Uses 12 · Used by 1

Statement usesTerm variable contexts of System F · One-step call-by-value evaluation · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms · Value forms of pure System F

Proof usesInstantiating the newest term binder of a term · Type substitution in System F terms · Instantiating the newest type binder of a type · Type-variable renaming in System F types · Canonical forms of function-typed values · Canonical forms of universally typed values

Used byType safety for closed well-typed terms

TheoremType preservation along evaluation sequences#✓fully proved

Every finite evaluation sequence preserves the exact type.

theorem preservation_steps (ht : Typing Γ t A) (hs : Steps t t') :
    Typing Γ t' A

Uses 7 · Used by 1

Statement usesTerm variable contexts of System F · Multi-step call-by-value evaluation · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesOne-step call-by-value evaluation · Type preservation for a call-by-value step

Used byType safety for closed well-typed terms

TheoremType safety for closed well-typed terms#✓fully proved

No term reachable from a closed well-typed term is stuck.

theorem safety {Γ : Ctx n 0} {t t' : Tm n 0}
    (ht : Typing Γ t A) (hs : Steps t t') :
    Value t' ∨ ∃ t'', Step t' t''

Uses 9

Statement usesTerm variable contexts of System F · One-step call-by-value evaluation · Multi-step call-by-value evaluation · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms · Value forms of pure System F

Proof usesType preservation along evaluation sequences · Progress for well-typed terms without free term variables

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.