Topic | TAPL Chapter# | Link | See also |
---|---|---|---|
0 untyped | 5 | Untyped λ Calculus | - |
1 simple | 9 | Simple Type Systems | - |
2 subtype | 15 | Subtyping | - |
3 rectype | 20 | Recursive Types | - |
4 polymorphism | 22 | Type reconstruction | Unification |
4 polymorphism | 23 | Universal Polymorphism | λ2, System F |
4 polymorphism | 24 | Existential Polymorphism | - |
4 polymorphism | 26 | Bounded Quantification | Fsub (popular since 80s) |
5 higher-order | 29 | Kinds and Type Operators | λω_, System Fω_ |
attapl:
- precise type analyses:
- type systems for low-level languages:
- applications of types to reasoning about computer programs:
- design of sophisticated module systems:
- ML-style type inference: