| Chapter 1 | |
| 1: | (**) Representing evaluation contexts |
| 2: | (*) Progress in lambda-calculus |
| 3: | (*) Printer for acyclic types |
| 4: | (*) Free type variables for recursive types |
| 5: | (**) Generalizable variables |
| 6: | (*) Non typability of fix-point |
| 7: | (*) Using the fix point combinator |
| 8: | (**) Type soundness of the fix-point combinator |
| 9: | (*) Multiple recursive definitions |
| 10: | (*) Fix-point with recursive types |
| 11: | (**) Printing recursive types |
| 12: | (**) Lambda-calculus with recursive types |
| Chapter 2 | |
| 13: | (**) Matching Cards |
| 14: | (***) Type soundness for data-types |
| 15: | (**) Data-type definitions |
| 16: | (*) Booleans as datatype definitions |
| 17: | (***) Pairs as datatype definitions |
| 18: | (**) Recursion with datatypes |
| 19: | (*) Mutually recursive definitions of abbreviations |
| 20: | (**) Recursion with references |
| 21: | (**) Type soundness of exceptions |
| 22: | (**) Recursion with exceptions |
| Chapter 3 | |
| 23: | (*) Self types |
| 24: | (**) Backups |
| 25: | (***) Logarithmic Backups |
| 26: | (**) Object-oriented strings |
| 27: | (**) Object types |
| 28: | (**) Unification for object types |
| 29: | Project —type inference for objects |
| 30: | Project —A widget toolkit |
| Chapter 4 | |
| 31: | Polynomials with one variable |
| Chapter 5 | |
| 32: | Project —A small subset of the FOC library |
| Chapter A | |
| 33: | (*) Unix commands true and false |
| 34: | (*) Unix command echo |
| 35: | (**) Unix cat and grep commands |
| 36: | (**) Unix wc command |