Formalisation of Goedel's System T in Coq
Coq
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Equivalence.v
Makefile
README
Semantics.v
Substitution.v
Syntax.v
Termination.v

README

This development formalises the notions from the first few lectures on
Type Theory Foundations at OPLSS 2011.

* Overview of the development:
** Syntax
   Defines the syntax of the language and some notations. Nothing fancy.
** Substitution
   Defines substitutions for de Bruijn indices. Pretty much the most boring
   thing possible.
** Semantics
   Defines static and dynamic semantics of the language, proves the standard
   properties: weakening, progress, preservation, etc. and lemmas needed by
   termination proof that are not related to logical relations.
** Termination
   Defines the reducibility relation and proceeds to prove head expansion
   and termination.
** Equivalence
   Defines contexts and context typings, observable equivalence and logical equivalence,
   and proves soundness of logical equivalence wrt observable equivalence. Provdies one
   example of a logical equivalence (x : ω ⊢ x ∼ x + 0 : ω).