A theory of type theories

类型理论的理论

• 批准号: EP/T000252/1
• 负责人: Benedikt Ahrens
• 金额: $ 33.33万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT000252%2F1
• 关键词: theory; type; theories

Today, people and businesses are reliant on computer systems everyday for a variety of services ranging from healthcare, banking, travel, communications etc. When these systems fail, the consequences are staggering on multiple levels, severely affecting the society and the economy of countries. In the UK, in 2018 alone, there were several high-profile failures: more than 30m O2 users (ranging from delivery companies to London transit authority) in the UK lost access to data services after a software glitch in Ericsson equipment; millions of TSB customers lost access to their online bank accounts after a failed software upgrade; NHS Wales was temporarily unable to access patient data; processors from Intel were found to be vulnerable to attacks where sensitive data could be stolen. The consequences of systems failures are only bound to be more severe in the future, as more and more aspects of our lives will be organised by automated systems such as self-driving vehicles. There is thus a pressing need for reliable and secure computer systems implementing the functionality we depend on in our daily lives. This includes the software, hardware the software is running on and the mathematical algorithms underlying the software.Computer tools, so-called "computer proof assistants" can help reasoning about the correctness of mathematical algorithms, of software, and of models of hardware. Different languages have been developed as a foundation for such tools, and a several proof assistants have been developed that check the correctness of user-provided proofs. So far, computer proof assistants of different kinds have been used to check the correctness of a wide range of results, from pure mathematics (eg, Kepler Conjecture, Feit-Thompson Theorem) to practical computer systems (eg, C compiler CompCert, certified ML implementation CakeML, and certified micro operating-system seL4).The language that forms the basis of many of today's computer proof assistants is "type theory". Recent advances in the understanding of type theory have led to the development of a wealth of variations and extensions of the original type theory -- extensions by domain-specific language constructions, such as guarded type theory, cohesive type theory, and many others. These extensions are analogous to domain-specific programming languages, with built-in primitives to construct, and reason about, mathematical objects of a specialized mathematical domain.Whenever a language is proposed as the foundation of a computer proof assistant, a translation from that language into a world of mathematical objects needs to be specified. Giving this translation rigorously is thus part of proving a mathematical statement in a computer proof assistant. However, it requires much work full of technical details, and thus is rarely done with sufficient care.A significant obstacle here is the lack of 'modularity' results for syntax extensions of type theory: when reasoning about an extension of a core syntax, for which a translation has already been established, it should be possible to specify a translation on the extended syntax by only specifying it on the extension - thus reusing the work of translating the core syntax. However, there is no mathematical theory for 'extending a translation' to an extended syntax: currently, whenever a new type theory is conceived, a translation has to be specified from scratch.In light of the plethora of new type theories currently being designed, there is hence a pressing need for a mathematical framework for the specification of, and reasoning about, type theories, with a particular focus on modularity.This is why we aim, in this project, to develop a mathematical theory of type theories that encompasses the type theories currently used in computer proof assistants. In the long term, we envision a proof assistant whose underlying type theory is configurable via an implementation of our mathematical theory.

今天，人们和企业每天都依赖计算机系统提供各种服务，包括医疗保健，银行，旅游，通信等，当这些系统出现故障时，后果在多个层面上令人震惊，严重影响社会和国家的经济。仅在2018年，英国就发生了几起备受瞩目的故障：超过3000万O2用户（从快递公司到伦敦交通管理局）在爱立信设备出现软件故障后无法访问数据服务;数百万TSB客户在软件升级失败后无法访问他们的在线银行账户; NHS威尔士暂时无法访问患者数据;英特尔的处理器被发现容易受到攻击，敏感数据可能被盗。系统故障的后果在未来只会更加严重，因为我们生活的越来越多方面将由自动驾驶汽车等自动化系统来组织。因此，迫切需要实现我们日常生活中所依赖的功能的可靠和安全的计算机系统。这包括软件、运行软件的硬件和软件底层的数学算法。计算机工具，所谓的“计算机证明助手”可以帮助推理数学算法、软件和硬件模型的正确性。已经开发了不同的语言作为这些工具的基础，并且已经开发了几个证明助手来检查用户提供的证明的正确性。到目前为止，不同类型的计算机证明助手已经被用来检查广泛的结果的正确性，从纯数学（例如，开普勒猜想，Feit-Thompson定理）到实际的计算机系统（例如，C编译器CompCert，认证ML实现CakeML和认证微操作系统sel 4）。对类型理论的理解的最新进展导致了原始类型理论的大量变体和扩展的发展--特定领域语言结构的扩展，如守护类型理论，内聚类型理论等。这些扩展类似于特定领域的编程语言，具有内置的原语来构造和推理特定数学领域的数学对象。每当一种语言被提议作为计算机证明助手的基础时，需要指定从该语言到数学对象世界的翻译。因此，严格地给出这种翻译是在计算机证明助手中证明数学陈述的一部分。然而，它需要大量的工作充满了技术细节，因此很少做足够的照顾。这里的一个重要障碍是缺乏“模块性”的结果类型理论的语法扩展：当推理核心语法的扩展时，已经为其建立了翻译，应该可以通过仅在扩展上指定它来在扩展语法上指定转换，从而重用转换核心语法的工作。然而，没有数学理论可以将翻译“扩展”为扩展的语法：目前，每当一个新的类型理论被构思出来时，一个翻译必须从头开始指定。鉴于目前正在设计的大量新类型理论，因此迫切需要一个数学框架来规范和推理类型理论，特别关注模块化。这就是为什么我们的目标，在这个项目中，开发一个数学理论的类型理论，包括类型理论目前使用的计算机证明助手。从长远来看，我们设想一个证明助手，其基础类型理论可以通过我们的数学理论的实现进行配置。

项目成果

Algebraic Presentations of Dependent Type Theories

依赖类型理论的代数表示

• DOI: 10.48550/arxiv.2111.09948
• 发表时间: 2021
• 作者: Ahrens B

B-SYSTEMS AND C-SYSTEMS ARE EQUIVALENT

B 系统和 C 系统是等效的

• DOI: 10.1017/jsl.2023.41
• 发表时间: 2023
• 期刊: The Journal of Symbolic Logic
• 作者: AHRENS B

Displayed Monoidal Categories for the Semantics of Linear Logic

线性逻辑语义的显示幺半群范畴

• DOI: 10.1145/3636501.3636956
• 发表时间: 2024
• 作者: Ahrens B

A Higher Structure Identity Principle

更高结构同一性原则

• 发表时间: 2020
• 作者: Ahrens B

Implementing a category-theoretic framework for typed abstract syntax

为类型化抽象语法实现类别理论框架

• DOI: 10.1145/3497775.3503678
• 发表时间: 2022
• 作者: Ahrens B