Abstract

A remarkable development in the foundations of mathematics has been the appearance of deep structural analogies between seemingly disparate subjects such as logic, category theory, lambda calculus, algebraic geometry, and algebraic topology. In this talk, Raymond Puzio will survey these analogies in an elementary fashion. Starting with basic notions and definitions, he will progress to such topics as the Curry-Howard correspondence between lambda calculus and intuitionistic logic, the Lambek-Scott correspondence between type theory and category theory, the homotopy interpretation of equality in type theory, proof relevance, and illustrate them with examples. This talk is intended for a general audience, so will be self-contained, not assume prior acquaintance with the subject, and focus on general concepts and motivation rather than on rigorous derivations and technical details.

Bio

Raymond Puzio obtained his Bachelor's degree in Physics at Columbia, where he had his first introduction to LISP in the basement of the math building, followed by a doctorate at Yale. Since then, he has been using his parentheses to help investigate such topics as general relativity, fractional calculus, and the origin of life. He has also been active in PlanetMath.org where, among other things he prepared an online version of the HoTT book and in the NYC HoTT reading group where he studied it.