PARTICIPANT SUPPORT FOR ATTENDANTS TO THE CONFERENCE: TYPE THEORY, HOMOTOPY THEORY AND UNIVALENT FOUNDATIONS

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

This grant is for participation in the conference "Type Theory, Homotopy Theory and Univalent Foundations", at the Centre de Recerca Matematica in Barcelona (Spain), September 23-27, 2013. The grant will enable selected mathematicians affiliated with U.S. institutions to participate in the conference. The allocation of funds will favor graduate students, postdocs, junior faculty, and faculty with no current NSF support. The topic of the conference are the recent connections discovered between type theory and homotopy theory based on the interpretation of identity types as path spaces. These connections provide a new topological intuition that facilitates working with type theories and allow for new computational tools for manipulating homotopy-theoretic structures. Furthermore, Voevodsky's Univalent Foundations program provides a solid logical basis for the practice of identifying isomorphic structures, common throughout mathematics even if it is not allowed by standard set-theoretic foundations. The topic of the conference has an unusually wide impact since it involves several areas: mathematical logic, theoretical computer science, homotopy theory and category theory. In particular, the developments offer a new perspective on computer-assisted formalization of mathematical proofs and verification of their correctness, which promises to benefit all mathematical endeavor, and further influence on design of programming languages. Conference web page: http://www.crm.cat/2013/ctype