All lectures (except March 1st) will take place from 2:30 – 3:30 p.m. in the Mathematics Department (Bldg. 380, Room 383-N). The March 1 lecture will take place from 1:00 – 2:00 p.m.

All four lectures will be devoted to Homotopy lambda calculus.

Abstract:

Homotopy lambda calculus is a kind of dependent type system which comes together with a very natural semantics (models) with values in the homotopy category. I hope that it can be used to develop foundations of mathematics which are intuitive and at the same time formal enough to be implemented in proof checkers. I will start with a brief introduction to the type systems for mathematicians. Then I will describe the homotopy lambda calculus which is an instance of such systems and discuss how one can use it to formalize pure mathematics.