toc.md

TOC

1. Introduction
2. Mathematical Preliminaries

I Untyped Systems

3. Untyped Arithmetic Expressions (arith)
4. An ML Implementation of Arithmetic Expressions (arith)
5. The Untyped Lambda-Calculus (fulluntyped)
6. Nameless Representation of Terms (fulluntyped)
7. An ML Implementation of the Lambda-Calculus (fulluntyped)

II Simple Types

8. Typed Arithmetic Expressions (tyarith)
9. Simply Typed Lambda-Calculus (fullsimple)
10. An ML Implementation of Simple Types (simplebool)
11. Simple Extensions (fullsimple)
12. Normalization
13. References (fullref)
14. Exceptions (fullerror)

III Subtyping

15. Subtyping (rcdsub, fullsub)
16. Metatheory of Subtyping (rcdsub, joinsub, bot)
17. An ML Implementation of Subtyping
18. Case Study: Imperative Objects (fullref)
19. Case Study: Featherweight Java

IV Recursive Types

20. Recursive Types (fullequirec, fullisorec)
21. Metatheory of Recursive Types equirec

V Polymorphism

22. Type Reconstruction (recon, fullrecon)
23. Universal Types (fullpoly, fullomega)
24. Existential Types (fullpoly)
25. An ML Implementation of System F
26. Bounded Quantification (fullfsub, fullfomsub)
27. Case Study: Imperative Objects, Redux (fullfsubref)
28. Metatheory of Bounded Quantification (purefsub, fullfsub)

VI Higher-Order Systems

29. Type Operators and Kinding (fullomega)
30. Higher-Order Polymorphism (fullomega)
31. Higher-Order Subtyping (fomsub, fullfomsub)
32. Case Study: Purely Functional Objects (fullupdate)