Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

October 2, 2006

Voevodsky on the Homotopy λ-Calculus

Posted by John Baez

After Vladimir Voevodsky won the Fields medal, his research took a surprising turn. Instead of applying homotopy theory to algebraic geometry, he began applying it to computer science. Now he has made this available:

This appeared on a mailing list for announcements on type theory in computer science. I thank Benoit Valiron for bringing this to my attention and preparing the above Postscript version - I couldn’t read Voevodsky’s original PDF file.

Does anyone have any clue about what Voevodsky is doing??? If so, please let me know!

It’s not easy for me to tell, but I can’t help but suspect that the idea of a homotopy λ\lambda-calculus is related to the project of categorifying the λ\lambda-calculus, which we’ve already discussed here. I plan to talk about that more in a while.

If you like this stuff, you may also enjoy the Types Forum, a moderated email forum focusing on Type Theory in Computer Science, with a broad view of the subject encompassing semantical, categorical, operational, and proof theoretical topics, as well as algorithmic issues and applications. Typical topics include:

Typed, untyped, or polymorphic lambda calculus; type checking, inference, and reconstruction; subtyping, dependent types, calculus of constructions, the lambda cube; linear logic, the Curry-Howard correspondence; recursive types; adequate and fully abstract models; domain theory; category theory; term reduction, normalization, confluence; abstract data types; type systems for object-oriented, concurrent, distributed, and mobile programming.

I believe Voevodsky’s note was posted not here but on the closely allied mailing list called Types-announce, which is for announcements only.

Posted at October 2, 2006 6:40 PM UTC

TrackBack URL for this Entry:

0 Comments & 0 Trackbacks

Post a New Comment