Week 1: Untyped Lambda Calculus (Lecture Slides 01, Exercise Set 01, Reduction Graph Examples)
Week 2: Intuitionistic Propositional Logic (Lecture Slides 02 and Appendix, Exercise Set 02, Natural Deduction Examples)
Week 3: Simply Typed Lambda Calculus (Lecture Slides 03, Abstract Reduction Systems)
Week 4: The Curry-Howard Isomorphism (Lecture Slides 04, Curry-Howard Examples)
Week 5: Lattices, Heyting Algebras, Boolean Algebras (Lecture Notes)
Week 6: Lambda-Mu Calculus and Classical Propositional Logic (Lecture Slides 06, Lambda-Mu Calculus Examples)
Week 7: Interlude on Unification (Lecture Slides 07, Type-Inference Examples)
Week 8: Classical First-Order Logic (Lecture Slides 08 (A)), Intuitionistic First-Order Logic (Lecture Slides 08 (B))
Week 9: Kripke Semantics for Propositional and First-Order Logic (Lecture Notes), Ordering Notions (Lecture Notes)
Week 10: Polymorphic Lambda Calculus (System F) (Lecture Slides 10), without alpha-conversion (Lecture Slides 10 (B))
Week 11: Pure Type Systems and the Lambda-Cube (Lecture Slides 11, Examples in CoC)
Week 12: Calculus of Inductive Constructions (Lecture Slides 12, Christine Paulin's Notes and Slides)
Week 13: Predicative Subsystems of F and F-omega (Lecture Slides 13)
Week 14: Unresolved Questions, Open Problems, Simpler Proofs (Lecture Slides 14)
Miscellaneous Material (mentioned or briefly presented in lecture, though not part of the course syllabus):
Coloring problems and Ramsey theory (posted with author's permission, Boaz Tsaban)
Tiny example without polymorphic recursion, with polymorphic recursion, with polymorphic recursion (+ some help from user)
Examples requiring polymorphic recursion at ranks higher than 2
Examples of first-order theories (lecture slides)
Examples of first-order structures (lecture slides), more examples of first-order structures (lecture slides)
Examples in second-order logic (lecture slides)
What Is a Model of the Lambda Calculus? (historical article by Albert Meyer)
Quantified Boolean Formulas (related to intuitionistic second-order propositional logic, lecture slides)
The Girard-Reynolds Isomorphism (by Philip Wadler)
Typability and Type Checking in System F (historical article by Joe Wells)
Alternative definitions of The Computable Number-Theoretic Functions (courtesy of IIT, lecture slides)
Alpha-Conversion and Typability (by Kfoury, Ronchi, Tiuryn, Urzyczyn)
Type Reconstruction in Finite-Rank Fragments of the Polymorphic Lambda-Calculus (by Kfoury, Tiuryn)
Stratified Polymorphism (by Leivant)
Tiny example with and without predicative polymorphism
Definable Functions in the Simply-Typed Lambda-Calculus (by Zakrzewski)
The references below, especially [LCHI], cover a substantial amount beyond the scope of this course. If we omit some of it in the Spring 2019 semester, it is because we want to devote about 1/3 of the 14-week semester to the use and pragmatics of interactive proof assistants. The material to be omitted is important in its own right and can be given its full due in a separate follow-up course (depending on students' interests and research plans).
Lectures on the Curry-Howard Isomorphism: [LCHI], not available for free download, although you can inspect the table of contents and about 200 pages out of 400 for the full text on your computer screen. Warning: Pirated versions of an earlier draft can be found on the Web; contents and organization of the earlier draft are different in many places from the published book. We will make copies of individual chapters to registered students and serious auditors; to request copies of individual chapters, click on droga do paranoi.
Dependent Types: [DT].
The material on foundations is divided into five parts. Parts 1, 2, and 3 will cover some of the chapters from the book [LCHI] in sequential order and with different levels of details; this is background material focusing on basic properties of the Untyped Lambda Calculus, the Simply Typed Lambda Calculus, and the simplest version of the Curry-Howard Isomorphism. This material will be covered at a brisk pace, with a presentation of the main concepts and results, leaving many details in the proofs for reading assignments and homework exercises.
Part 4 will be covered at a slower pace and more in depth, stressing topics related to Dependent Types, Calculus of Constructions, and Calculus of Inductive Constructions -- which all form the essential foundations of the four automated systems under consideration.
Part 5 is a very brief introduction to Homotopy Type Theory, just an appetizer, only covered time permitting; it is somewhat unrelated to the material in the preceding parts of the course but, according to its luminaries, promises to play a big role in future developments of interactive proof assistants.
Below are the reading sources for the five parts described above:
[LCHI, Chapt 1, Chapt 2, Chapt 3], mostly background material on the Lambda Calculus and Simple Type Theory.
[LCHI, Chapt 4] without Sections 4.6 and 4.7, first introduction to the Curry-Howard Isomorphism.
[LCHI, Chapt 6, Chapt 8] extending the Curry-Howard Isomorphism to Classical Propositional Logic and Intuitionistic First-Order Logic.
[LCHI, Chapt 11, Chapt 13, Chapt 14], mixed with additional material on Dependent Types from [DT], and additional material on the Calculus of Inductive Constructions from [CIC_1] and [CIC_2].
[HoTT_1] and [HoTT_2], brief incursion into Homotopy Type Theory.