The taming of the Rew: A type theory with computational assumptions
In: Proceedings of the ACM on Programming Languages, 5(POPL) Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, ACM, 2021, POPL 2021, ⟨10.1145/3434341⟩ Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩; (2021)
Online
unknown
Zugriff:
International audience; Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logical principles in those systems, it is common to appeal to axioms to postulate their existence. However, one can only postulate the bare existence of an axiom, not its computational behaviour. Instead, users are forced to postulate equality proofs and appeal to them explicitly to simplify expressions, making axioms dramatically more complicated to work with than built-in primitives. On the other hand, the equality reflection rule from extensional type theory solves these problems by collapsing computation and equality, at the cost of having no practical type checking algorithm. This paper introduces Rewriting Type Theory (RTT), a type theory where it is possible to add computational assumptions in the form of rewrite rules. Rewrite rules go beyond the computational capabilities of intensional type theory, but in contrast to extensional type theory, they are applied automatically so type checking does not require input from the user. To ensure type soundness of RTT-as well as effective type checking-we provide a framework where confluence of user-defined rewrite rules can be checked modularly and automatically, and where adding new rewrite rules is guaranteed to preserve subject reduction. The properties of RTT have been formally verified using the MetaCoq framework and an implementation of rewrite rules is already available in the Agda proof assistant.
Titel: |
The taming of the Rew: A type theory with computational assumptions
|
---|---|
Autor/in / Beteiligte Person: | Tabareau, Nicolas ; Cockx, Jesper ; Winterhalter, Théo ; Delft University of Technology (TU Delft) ; Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N) ; IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique) ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire des Sciences du Numérique de Nantes (LS2N) ; European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015) ; Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE) ; Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT) ; Université de Nantes - Faculté des Sciences et des Techniques ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - Faculté des Sciences et des Techniques |
Link: | |
Quelle: | Proceedings of the ACM on Programming Languages, 5(POPL) Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, ACM, 2021, POPL 2021, ⟨10.1145/3434341⟩ Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩; (2021) |
Veröffentlichung: | 2021 |
Medientyp: | unknown |
ISSN: | 2475-1421 (print) |
Schlagwort: |
|
Sonstiges: |
|