LIPIcs.ITP.2024.26.pdf
- Filesize: 0.75 MB
- 18 pages
Document
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
Authors
Yann Leray 
,
Nicolas Tabareau ,
Théo Winterhalter
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Cite AsGet BibTex
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.26
https://doi.org/10.4230/LIPIcs.ITP.2024.26
Abstract
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
Keywords
- type theory
- dependent types
- rewrite rules
- type preservation
- Coq
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Andrej Bauer and Anja Petković Komel. An extensible equality checking algorithm for dependent type theories. Logical Methods in Computer Science, Volume 18, Issue 1, January 2022. URL: https://doi.org/10.46298/lmcs-18(1:17)2022.
- Frédéric Blanqui. Type Safety of Rewrite Rules in Dependent Types. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Schloss-Dagstuhl - Leibniz Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.13.
- Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The taming of the rew: A type theory with computational assumptions. Proceedings of the ACM on Programming Languages, 5(POPL):60:1-60:29, January 2021. URL: https://doi.org/10.1145/3434341.
- Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, pages 50-66, Berlin, Heidelberg, 1990. Springer. URL: https://doi.org/10.1007/3-540-52335-9_47.
- Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
- Thiago Felicissimo. Generic bidirectional typing for dependent type theories. In Stephanie Weirich, editor, Programming Languages and Systems, pages 143-170, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-57262-3_6.
- Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages, 3(POPL):3:1-3:28, January 2019. URL: https://doi.org/10.1145/3290316.
-
Jean-Yves Girard. Interprétation Fonctionnelle et Élimination Des Coupures de l'arithmétique d'ordre Supérieur. PhD thesis, Université Paris VII, 1972.
- Antonius J. C. Hurkens. A simplification of Girard’s paradox. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, pages 266-278, Berlin, Heidelberg, 1995. Springer. URL: https://doi.org/10.1007/BFb0014058.
- Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In DROPS-IDN/v2/Document/10.4230/LIPIcs.ITP.2021.24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.24.
-
Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory, volume 32. Citeseer, 2007.
- Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option an exceptional type theory. In ESOP 2018 - 27th European Symposium on Programming, volume 10801 of LNCS, pages 245-271, Thessaloniki, Greece, April 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
- Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
- Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. PACMPL, 4(POPL), 2020. URL: https://doi.org/10.1145/3371076.
- The Coq Development Team. The Coq Proof Assistant. Zenodo, June 2023. URL: https://doi.org/10.5281/zenodo.8161141.
- Beta Ziliani and Matthieu Sozeau. A unification algorithm for Coq featuring universe polymorphism and overloading. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 179-191, New York, NY, USA, August 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2784731.2784751.