Translations between Type Theories

类型理论之间的翻译

• 批准号: EP/Z000602/1
• 负责人: Nicolai Kraus
• 金额: $ 218.91万
• 依托单位: University of Nottingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2025
• 资助国家: 英国
• 起止时间: 2025 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FZ000602%2F1
• 关键词: Translations; between; Type; Theories

Dependent type theories are logical systems that enable us to formally verify theorems and certify the correctness of software. An example of a commercial application is Google's encryption used by the web browser Chrome, while computer-based proof assistants can verify modern mathematics. In recent years, new type theories have started to even serve as highly specialised languages for the study of complex mathematical disciplines.Around 2010, the research field was revolutionised by the inception of homotopy type theory, a variation that combines insights from logic, programming, and abstract homotopy theory. Inspired by this, the last decade has seen a plethora of new type theories including cubical, cartesian cubical, modal, spatial, cohesive, directed, and two-level type theory. Their relationships with each other are almost completely unknown and a success in one subfield has a priori limited consequences for other subfields, significantly hindering the progress of the research area as a whole.The project Triple-T will construct translations between type theories, unifying the efforts of different communities. This will be achieved by creating multi-level type theory, a framework that combines the advantages of individual (currently incompatible) theories and presents a radically new approach to studying correlations known as conservativity of extensions. As a side effect, it will greatly benefit the design of new type theories by determining in advance which features are needed in order to preserve certain desired properties.While the project will provide the field with powerful tools that can be applied immediately, it also has the potential for enormous long-term impact. By making it possible to combine the most useful aspects of currently incompatible systems, Triple-T will permanently speed up the development of new type theories and more advanced proof assistants, the formalisation of mathematical results, and the formal verification of software.

依赖类型理论是逻辑系统，使我们能够正式验证定理并证明软件的正确性。商业应用的一个例子是网络浏览器 Chrome 使用的谷歌加密，而基于计算机的证明助手可以验证现代数学。近年来，新型类型理论甚至开始成为研究复杂数学学科的高度专业化语言。 2010 年左右，同伦类型理论的诞生彻底改变了该研究领域，同伦类型理论是一种结合了逻辑、编程、和抽象同伦论。受此启发，过去十年出现了大量新型理论，包括三次、笛卡尔三次、模态、空间、内聚、定向和两级类型理论。它们之间的关系几乎完全未知，一个子领域的成功对其他子领域的先验有限影响，极大地阻碍了整个研究领域的进步。 Triple-T 项目将构建类型理论之间的翻译，统一不同社区的努力。这将通过创建多层次类型理论来实现，该框架结合了各个（当前不兼容）理论的优点，并提出了一种全新的方法来研究称为扩展保守性的相关性。作为副作用，通过提前确定需要哪些特征来保留某些所需的属性，它将极大地有利于新型理论的设计。虽然该项目将为该领域提供可以立即应用的强大工具，但它也有产生巨大长期影响的潜力。通过将当前不兼容系统的最有用的方面结合起来，Triple-T 将永久加速新型理论和更先进的证明助手的开发、数学结果的形式化以及软件的形式化验证。