Type systems and lambda calculi
Typed lambda calculi and type inference: the simply typed lambda calculus (syntax, substitution, normalization, logical relations, normalization by evaluation, elaboration, its models), lambda calculus with references and type safety, and Hindley-Milner let-polymorphism with Algorithm W.
- Calculus of constructions
- Hindley–Milner type inference
- Simply typed lambda calculus
- System F
- System Fω
- Operational semantics of the simply typed lambda calculus
- Denotational semantics of the simply typed lambda calculus
- Normalization by evaluation
- Normalization of the simply typed lambda calculus
- Type checking for the simply typed lambda calculus
- Lambda calculus with references
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.