An axiom-free model for curry-style System F Omega (PTS with type-level computation and polymorphism, but without dependent types) mechanized in Coq.
The f_omega_normalize function in semantics.v effectively gives you a normalizer for well-typed F omega terms.
The default fomega branch contains the SN proof. The parametricity proof, based on Harper's notes Reynolds’s Parametricity Theorem, Directly, can be found in the zigzag branch.
Coq's impredicative sort Prop is necessary for the proof to go through because the object language is impredicative. The lack of impredicativity from the metalanguage is the reason why the substitution function in Agda development can't be proven to be terminating.
I only proved strong normalization for terms but not for types. The latter is quite easy because type-level computation is simply typed and can be proven independently from the SN result for terms.
The strong normalization proof can be extended to a strong normalization proof for Calculus of Constructions (CoC) by translating CoC terms to F Omega terms. The translation proof does not require impredicativity and can be carried out in Agda and Coq alike. Note that this translation proof is no longer possible the moment you extend CoC with large elimination because the translation fundamentally relies on the erasure of terms appearing in types (which also means CoC is a bad example for understanding how to model the mutual dependency between terms and types).
Here are some references I used for this development:
- A short and flexible proof of strong normalization for the calculus of constructions
- Coq in Coq
- POPLmark Reloaded
The Coq files are stored under the theories directory.
The Autosubst2 directory contains the syntax files generated by the autosubst tool. The syntax specification can be found in syntax.sig. Autosubst generates the substitution functions and tactics for proving equalities about substitutions.
par.v contains the reduction relations for types and terms. It also includes an inductive characterization of strongly normalizing (and neutral) terms.
typing.v contains the typing judgments of the language, including type well-formedness (TyWt) and term well-typedness (Wt).
semantics.v contains the semantic interpretations for kinds (int_kind) and types (int_type). The fundamental theorem is named soundness and the final strong normalization result f_omega_sn.
- coq-hammer-tactics 1.3.2
- stdpp 1.10.0
- coq 8.19.2
- coq-equations 1.3
- coq-autosubst-ocaml 1.1