1. Introduction
3. Foundations
4. 1. Type Systems
6. Algorithm W
7. 2. Lambda Calculus
8. 3. Type Inference
9. 4. Examples
11. Type Classes
12. 5. Overview
13. 6. Implementation
14. 7. Dictionary Elaboration
15. 8. Examples
17. System F
18. 9. System F
19. 10. Type Checker
20. 11. Examples
22. System Fω
23. 12. System Fω
24. 13. Language Design
25. 14. Lexer and Parser
26. 15. Type Checking
27. 16. Pattern Coverage
28. 17. Code Generation
29. 18. Examples
31. Refinement Types
32. 19. Overview
33. 20. Implementation
34. 21. Examples
36. Calculus of Constructions
37. 22. Overview
38. 23. Dependent Types
39. 24. Type System
40. 25. Inductive Types
41. 26. Type Rules
42. 27. Universe Polymorphism
43. 28. Constraint Solving
44. 29. Examples
46. Row Polymorphism
47. 30. Overview
48. 31. Implementation
49. 32. Examples
51. Row Effects
52. 33. Overview
53. 34. Implementation
54. 35. Examples
56. Call-by-Push-Value
57. 36. Overview
58. 37. Implementation
59. 38. Examples
61. References
62. 39. References