Perhaps this should be advertised on the list. Thanks, Jean-Pierre Marquis Professeur agrégé Département de philosophie Université de Montréal C.P. 6128, succ. Centre-ville Montréal Qc Canada H3C 3J7 tél.: 514-343-2029 fax: 514-343-7899 Début du message réexpédié :
De: Grigori Mints <mints@csli.stanford.edu> Date: 8 février 2006 21:44:58 GMT-05:00 À: logic@cs.Stanford.EDU, logical-methods@lists.Stanford.EDU Objet: Voevodsky
See http://math.stanford.edu/distinguished_voevodsky.htm The first two 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.
The titles of the last two lectures will be announced later.