Dear All, You may know that Vladimir Voevodsky is interested in lambda-calculus. http://www.math.ias.edu/~vladimir/Site3/home.html He also gave a talk at the CMU two months ago on Martin-Lof type theory in relation to homotopy theory. The notes are on its web-page. I would like to thank Jean-Pierre Marquis for drawing my attention to that. Best, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ]