The Mathematics Research Center presents
Distinguished Lecturer Series
Professor Vladimir Voevodsky
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.
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.
For a list of previous “Distinguished Lecturers,” see http://math.stanford.edu/mrc-support.htm
To subscribe to the Stanford Mathematics’ Seminar mailing list, send e-mail