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

与会者对与会者的支持：类型论、同伦论和统一基础

基本信息

批准号：
1324746
负责人：
Steven Awodey
金额：
$ 2.1万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2013
资助国家：
美国
起止时间：
2013-04-15 至 2014-03-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1324746&HistoricalAwards=false
关键词：
PARTICIPANT SUPPORT ATTENDANTS CONFERENCE TYPE

项目摘要

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

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