Fwd: Voevodsky

Fwd: Voevodsky

[Marquis Jean-Pierre]

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.
>
>
>