Implementations of and reasonings about the following languages:
| name | description | common parlence | resources |
|---|---|---|---|
| λ | simply-typed λ-calculus | STλC | |
| λ2 | λ with type polymorphism | System F | |
| λω | λ2 with type constructors | System Fω | |
| λΠ | λ with dependent types | ||
| λΠω | λΠ with type constructors | Calculus of Constructions | Calculus of Constructions [wiki] |
| λS | λΠω with self types | System S | Self Types for Dependently Typed Lambda Encodings [paper] |
| λID | λΠω with inductive datatypes | Calculus of Inductive Constructions | |
| λCD | λΠω with coinductive datatypes | Calculus of Coinductive Constructions | |
| λPID | predicative λΠω with inductive datatypes | Predicative Calculus of Coinductive Constructions |
λ: Simply-typed λ-calculus.
Language/Lambda/ contains an intrinsically-typed implementation. Based on Programming Language Foundations in Agda –– DeBruijn: Intrinsically-typed de Bruijn representation.
Tasks.
- Grammar
- Typing
- Reducing
- Examples
- simples
- Church numerals
λ2: λ with type polymorphism (System F).
Lambda/Lambda2/ contain an intrinsically-typed implementation. Based on System F in Agda for Fun and Profit.
Tasks.
- Kinding
- properties of
_≅ₛ_ - properties of
rename-⊨ - properties of
reflect - properties of
reify - interactions between
rename,substitute,extend,evaluate,reflect,reify, and_≅ₛ_ - properties of
_≅ₛ_ - properties of
_≅ₑ_ - completeness
- stability
- interactions between
rename,substitute, weakenings, and single substitutions
- properties of
- Typing
- Normal Typing
- normalization lemmas
-
normalize-Typecases:-
`fold -
`unfold
-
-
progresscases:-
_`∙♯_ -
`unfold
-
- Type Erasure
-
erase-normalize-Type-≡ - erase-substitution lemmas
-
TODO
TODO
TODO
TODO
TODO
TODO
TODO
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent