License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.24
URN: urn:nbn:de:0030-drops-163059
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16305/
Blanqui, Frédéric
Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity
Abstract
The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi.
BibTeX - Entry
@InProceedings{blanqui:LIPIcs.FSCD.2022.24,
author = {Blanqui, Fr\'{e}d\'{e}ric},
title = {{Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {24:1--24:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16305},
URN = {urn:nbn:de:0030-drops-163059},
doi = {10.4230/LIPIcs.FSCD.2022.24},
annote = {Keywords: logical framework, type theory, type universes, rewriting}
}
