The Mathematics Research Center presents

Distinguished Lecturer Series

Photo of Vladimir Voevodsky

Professor Vladimir Voevodsky
(Institute for Advanced Study, Princeton)

  • Thursday, February 16
  • Thursday, February 23
  • Wednesday, March 1
  • Thursday, March 9

    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

To subscribe to the Stanford Mathematics’ Seminar mailing list, send e-mail
to announce “at”