Permalink
Cannot retrieve contributors at this time
Fetching contributors…
Cannot retrieve contributors at this time
| 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 : ω). |