1. Introduction
3. Foundations
4. 1. Type Systems
6. Algorithm W Implementation
7. 2. Lambda Calculus
8. 3. Type Inference
9. 4. Examples
11. System F Type Checker
12. 5. System F
13. 6. Type Checker
14. 7. Examples
16. System F-ω Type Checker
17. 8. System F-ω
18. 9. Language Design
19. 10. Lexer and Parser
20. 11. Type Checking
21. 12. Examples
23. Calculus of Constructions
24. 13. Overview
25. 14. Dependent Types
26. 15. Type System
27. 16. Inductive Types
28. 17. Type Rules
29. 18. Universe Polymorphism
30. 19. Constraint Solving
31. 20. Examples
33. Appendices
34. 21. Bibliography