# CIS 6700: Type Systems - Spring 2025

## Homeworks

Exercise numbers refer to TAPL.

| # | Homework | Due |
| - | -------- | --- |
| 1 | Formal definition of substitution on de Bruijn terms | 27 January |
| 2 | 3.5.16, 3.5.17 | 3 February |
| 3 | [Exercise 2](https://www.cs.cmu.edu/~rwh/courses/atpl/pdfs/tait.pdf); largest and smallest saturated sets | 10 February |
| 4 | 13.3.1, 13.5.8 | 19 Feburary |
| 5 | 15.3.6, 16.1.3, 16.2.5, 16.2.6, 16.3.2 | 24 Feburary |
| 6 | Barendregt's or Gallier's normalization proof | 5 March |
| 7 | 22.3.9, 22.3.10, 22.4.6, 22.5.5 | 17 March |
| 8 | 26.3.5, 26.4.11, 28.2.3, 28.7.1 | 26 March |