- Lecture I (Introduction to typed lambda calculi)
- Slides
- Associated files: Barendregt 1992 and an SN proof (Appendix 2 of Hindly & Seldin 1986)

- Lecture II (Propositions as types)
- Slides
- Associated file: Howard 1969

- Lecture III (Computational meaning and inductive types)
- Slides
- Associated file: Intro to J volume on proof-theoretic semantics

- Lecture IV (Subtyping in type theoreies with canonical objects)
- Slides
- Associated files: Mitchell 1991, Luo 1998 on coercive subtyping and Aspinall & Compagnoni 2001 on subtyping dependent types

- Lecture V (Type-theoretical semantics)
- Slides
- Associated files: Montague 1973, Portner & Partee 2002 and Luo 2010 SALT20 paper

Back to Zhaohui Luo's home page.