The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
In: https://inria.hal.science/hal-04511667 ; 2024, 2024
Online
report
Zugriff:
In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them.Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour.While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as type preservation.In this paper, we present an implementation of rewrite rules on top of the Coq proof assistant, together with a modular criterion to ensure that the added rewrite rules preserve typing. This criterion, based on bidirectional type checking, is formally expressed in PCUIC --- the type theory of Coq recently developed in the MetaCoq project.
Titel: |
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
|
---|---|
Autor/in / Beteiligte Person: | Leray, Yann ; Gilbert, Gaëtan ; Tabareau, Nicolas ; Winterhalter, Théo ; Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Institut National de Recherche en Informatique et en Automatique (Inria)-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)-NANTES UNIVERSITÉ - École Centrale de Nantes (Nantes Univ - ECN) ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST) ; Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ) ; IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom Paris (IMT) ; 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) ; Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) |
Link: | |
Zeitschrift: | https://inria.hal.science/hal-04511667 ; 2024, 2024 |
Veröffentlichung: | HAL CCSD, 2024 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|