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

该基金用于参加2013年9月23日至27日在西班牙巴塞罗那的deRecerca Matematica中心举行的“类型理论、同伦理论和单价基础”会议。这笔拨款将使与美国机构有联系的数学家能够参加这次会议。资金的分配将有利于研究生、博士后、初级教师和目前没有NSF支持的教师。会议的主题是最近发现的类型理论和同伦理论之间的联系，基于对同一性类型作为路径空间的解释。这些联系提供了一种新的拓扑直觉，便于与类型理论一起工作，并允许使用新的计算工具来操作同伦理论结构。此外，Voevodsky的一元基础程序为识别同构结构的实践提供了坚实的基础，这在整个数学中很常见，即使标准集合论基础不允许。本次会议的主题涉及数学逻辑、理论计算机科学、同伦论和范畴论等多个领域，影响非常广泛。特别是，这些发展为计算机辅助数学证明的形式化及其正确性验证提供了一个新的视角，这有望使所有数学努力受益，并进一步影响编程语言的设计。会议网页：http://www.crm.cat/2013/ctype

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