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.

依赖类型的理论是逻辑系统，使我们能够正式验证定理并证明软件的正确性。商业应用程序的一个示例是Web浏览器Chrome使用的Google加密，而基于计算机的证明助手可以验证现代数学。近年来，新型理论甚至开始充当高度专业的语言，用于研究复杂的数学学科。2010年，研究领域通过同型类型理论的启动而彻底改变了研究领域，这种变化结合了逻辑，编程和抽象同拷贝理论的洞察力。受到这一点的启发，过去十年中看到了许多新型理论，包括立方体，笛卡尔立方体，模态，空间，凝聚力，定向和两级类型的理论。他们彼此之间的关系几乎是完全未知的，在一个子领域的成功对其他子领域的后果有限，这极大地阻碍了整个研究领域的进步。这将通过创建多层型理论来实现，该理论结合了个体（当前不兼容的）理论的优势，并提出了一种研究相关性的新方法，称为扩展的保守性。作为副作用，它将通过预先确定需要哪些功能来保留某些所需的属性，从而极大地使新类型理论的设计受益。虽然该项目将为该领域提供可立即应用的强大工具，但它也具有巨大的长期影响。通过结合当前不兼容系统的最有用方面，Triple-T将永久加快新型理论和更高级的证明助手的发展，数学结果的形式化以及软件的正式验证。