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: www.crm.cat/2013/ctype
at the Center for Mathematical Research of the Autonomous University in Barcelon, Spain. Graduate students and postdocs received training via a week-long series of dedicated tutorial lectures, enabling them to participate more fully and effectively in the subsequent week of research-oriented lectures of the main conference. The research presented at the conference will likely have an impact on mathematics through the development of computerized proof assistants implementing new foundations, and also on computer science through the use of homotopical methods in program verification. In addition to the training of graduate students and postdocs, a research collaboration was established between the research group at CMU and that in Barcelona, likely leading to future collaboration and possibly longer-term visits for the purpose of collaborative research. The slides of the lectures are avalable online, and several research publications will result from the lectures given at the conference. Participants supported were from the following institutions: Carnegie Mellon, Weslyan, University of Washington, Harvard, MIT, University of Pittsburgh, University of Illinois Urbana-Champaign, Johns Hopkins.
