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

点击翻译按钮获取中文摘要

This grant is for participation in the conference "Type Theory,Homotopy Theory and Univalent Foundations", at the Centre deRecerca 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 allocationof funds will favor graduate students, postdocs, junior faculty,and faculty with no current NSF support.The topic of the conference are the recent connectionsdiscovered between type theory and homotopy theory based on theinterpretation of identity types as path spaces. Theseconnections provide a new topological intuition that facilitatesworking with type theories and allow for new computational toolsfor manipulating homotopy-theoretic structures. Furthermore,Voevodsky's Univalent Foundations program provides a solidlogical basis for the practice of identifying isomorphicstructures, common throughout mathematics even if it is notallowed by standard set-theoretic foundations.The topic of the conference has an unusually wide impact sinceit involves several areas: mathematical logic, theoreticalcomputer science, homotopy theory and category theory. Inparticular, the developments offer a new perspective oncomputer-assisted formalization of mathematical proofs andverification of their correctness, which promises to benefit allmathematical endeavor, and further influence on design ofprogramming languages.Conference web page: http://www.crm.cat/2013/ctype