Course Background:
Constructive logic and type theory provide foundations for constructive mathematics. There is a close connection between constructive and computational views. This connection between logic and computation has applications in computer science. For example, proof assistants such as Coq and Nuprl, type structure of modern programming languages are founded on these ideas.
Recently, homotopy type theory has provided an application of these ideas to mathematics also. Namely, some simple reults of algebraic topology have been formalized in a type theory and proved using proof assistants.
The aim of this course will be to give a self contained introduction to these topics.
Course Contents:
We plan to cover the following topics.
1. Natural deduction for propositional logic, Curry Howard isomorphism.
2. Simply Typed lambda calculus, its extensions with polymorphism and dependent types. Normalization theorems.
3. Some issues in semantics, an introduction to category theory to the extent needed in semantical issues.
4. Intuitionistic Type theory of Martin Lof. Proof relevance, extensional vs intensional, identity types. Path induction. Groupoid model for intensional type theory.
5. An introduction to homotopy type theory. Type equivalence and univalence. higher inductive types. Some recent developments like computational type theory will be explored if time permits.
The course will be theoretical. It will encourage active involvement of students in terms of reading papers, students presentations and discussions. These will also be main part of evaluation.
Some References:
1. Jean Yves Girard, Paul Taylor and Yves Lafont. 1989. Proofs and Types. Cambridge University Press.
2. Bengt Nordström, Kent Petersson, Jan M. Smith. 1990. Programming in
Martin-Löf ’s Type Theory, An Introduction. Oxford University Press.
3. The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent
Foundations of Mathematics. https://homotopytypetheory.org/book.
4. Research papers.