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:
- Vladimir Voevodsky, A very short note on homotopy -calculus, Sept. 27, 2006.
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 -calculus is related to the project of categorifying the -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.