Lectures on Type Theory (Zhaohui Luo; Tsinghua University, April 2011)

Lecture slides and associated distributions

• 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