eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-28
11:1
11:19
10.4230/LIPIcs.TYPES.2022.11
article
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families
Dubois, Catherine
1
https://orcid.org/0000-0002-9477-8109
Magaud, Nicolas
2
https://orcid.org/0000-0002-9477-4394
Giorgetti, Alain
3
https://orcid.org/0000-0002-0990-9611
Samovar, ENSIIE, 1 square de la résistance, 91025 Évry-Courcouronnes, France
Lab. ICube UMR 7357 CNRS Université de Strasbourg, 67412 Illkirch, France
Université de Franche-Comté, CNRS, Institut FEMTO-ST, F-25030 Besançon, France
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restriction property are much easier to deal with.
In this work, we study several families related to lambda terms, among which Motzkin trees, seen as lambda term skeletons, closable Motzkin trees, corresponding to closed lambda terms, and a parameterized family of open lambda terms. For each of these families, we define two different representations, show that they are isomorphic and provide tools to switch from one representation to another. All these datatypes and their associated transformations are implemented in the Coq proof assistant. Furthermore we implement random generators for each representation, using the QuickChick plugin.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-types2022/LIPIcs.TYPES.2022.11/LIPIcs.TYPES.2022.11.pdf
Data Representations
Isomorphisms
dependent Types
formal Proofs
random Generation
lambda Terms
Coq