WHY: Description and Objectives
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 for both Philosophy, Math, and CS. After having a whole picture of type theory, we will look at some the recent research about type theory.
There are three parts in the course, first part is to build a 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. In the last part of the course we will go through some research topics relevant to type theory.
WHAT: Setups
Pre-req (not required, but highly recommended)
You would notice that the following recommendations could be fulfilled if you have taken my LGC-203/MTH/CSC: Logics in Computer Science, and you will be comfortable with the course after taking it.
- Experiences in Classical First-Order Logic (Syntax, Semantics, Truth Table)
- Experiences in Natural/Structural Induction (Peano Arithmetics, Graph Theory)
- Experiences in Coding (It is highly recommended to set up LEAN in your computer for learning and final project).
Course Time and Office Hour
- Course time: Typically
09:30-11:30once a week for graduate or09:30-10:45/14:00-15:15twice a week for undergrad. - Office Hour: Typically an hour in person just after the class or online by reservation with email.
Materials and Resources (not required)
- Type Theory: Nederpelt, R., & Geuvers, H. (2014). Type Theory and Formal Proof: An Introduction. Cambridge University Press.
- LEAN:
Grading
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
- Homework 1 (Due Week 03): PDF, $\TeX$
- Homework 2 (Due Week 05): PDF, $\TeX$
- Exam 1 (Week 05 in class): PDF, $\TeX$
- Homework 3 (Due Week 08): PDF, $\TeX$
- Coding Part, you need to attach a screenshot to show your code compiled as the first part of the question. If you find the coding confusing, you may do some practices start from Dependent Type or even Type Theory in LEAN first. Notice that you could turn the
Rulesat the right top tononefor efficiency and convenience.
- Coding Part, you need to attach a screenshot to show your code compiled as the first part of the question. If you find the coding confusing, you may do some practices start from Dependent Type or even Type Theory in LEAN first. Notice that you could turn the
- Homework 4 (Due Week 10): PDF, $\TeX$
- Exam 2 (Week 10 in class): PDF, $\TeX$
- (Homework 5 (Due Week 13): PDF, $\TeX$)
- Final Project or Final Paper (Due Last Class)
- Final Project
- Final Paper
HOW: Schedule
- 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 & Exam 1
- Week 06: STLC in LEAN & some syntax and semantics in LEAN
- Week 07: Dependent 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 & Exam 2
- Week 10+: Research Topics: Monad (StateM in LEAN) & Type and Effect System & FPIL
- Week 10+: Research Topics: Type Theory & Russell Paradox (Axiom & ZFC & Models)
- Week 10+: Research Topics: Homotopy Type Theory
- Week 10+: Research Topics: Philosophical logic