Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Formalisation of Goedel's System T in Coq
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
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 : ω).