WHY: The reason for setting up the course

The goal for the course is to understand basic type theory, the theoretical foundation for LEAN, and know how to use LEAN as a proof assistant. After have a whole picture of type theory, we will look at some the recent researches about type theory.

There are three parts in the course, first part is build the fundamental basis for lambda-calculus and type theory, second part is to deepen the understanding of type theory, then understand how LEAN work, and also learn how to use LEAN as a proof assistant. The last part of the course we will go through some research topics relevant to type theory.

WHAT: The setup

Course Time and Office Hour

• Course time: Typically 09:30-11:30 or 09:30-10:45/14:00-15:15
• Office Hour: Typically an hour in person just after the class or online by reservation with email.

Grading

Adopting bonus points system, curving will only be applied in a very few cases.

40% Homework + 15% 1st Exam + 20% 2nd Exam + 25% Final Project/Paper

HOW: Syllabus

• Week 01: Intro & Logic Basics & structural induction
• Week 02: Untyped Lambda-calculus & Church Rosser
• Week 03: STLC & Curry Howard in IPL & weak normalization thm
• Week 04: and, or, not in IPL, completeness, limitations for STLC
• Week 05: Review & Midterm
• Week 06: STLC in LEAN & some syntax and semantics in LEAN
• Week 07: SOTLC with term depends on type, inductive in LEAN, linkedlist, stack, and btree
• Week 08: System T and System F, more proofs in LEAN
• Week 09: Total Dependency Hierarchy, LEAN, completeness and expressiveness
• Week 10: Review & Midterm 2
• Week 11: Research Topics: Monad (StateM in Lean) & Type and Effect System & FPIL
• Week 12: Research Topics: Type Theory & Russell Paradox (Axiom & ZFC & Models)
• Week 13: Research Topics: Homotopy Type Theory
• Week 14: Research Topics: Philosophical logic