LIPIcs.TYPES.2022.11.pdf
- Filesize: 0.66 MB
- 19 pages
Document
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families
Authors
Catherine Dubois 
,
Nicolas Magaud ,
Alain Giorgetti
-
Part of:
Volume:
28th International Conference on Types for Proofs and Programs (TYPES 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-28
File
Document Identifiers
Author Details
Cite As Get BibTex
Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.11
Abstract
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Lambda calculus
- Theory of computation → Logic and verification
- Theory of computation → Type theory
Keywords
- Data Representations
- Isomorphisms
- dependent Types
- formal Proofs
- random Generation
- lambda Terms
- Coq
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
Supplementary Materials
-
Software (Source Code)
https://github.com/magaud/postTYPES2022
browse
archived version
References
- Maciej Bendkowski, Olivier Bodini, and Sergey Dovgal. Statistical Properties of Lambda Terms. The Electronic Journal of Combinatorics, 26(4):P4.1, October 2019. URL: https://doi.org/10.37236/8491.
-
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development, Coq'Art : Thealculus of Inductive Constructions. Springer-Verlag, Berlin/Heidelberg, May 2004. 469 pages.
- Olivier Bodini and Paul Tarau. On uniquely closable and uniquely typable skeletons of lambda terms. In Fabio Fioravanti and John P. Gallagher, editors, Logic-Based Program Synthesis and Transformation. LOPSTR 2017, volume 10855 of Lecture Notes in Computer Science, pages 252-268. Springer, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-94460-9_15.
- Koen Claessen and John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, volume 35 of SIGPLAN Not., pages 268-279. ACM, New York, 2000. URL: https://doi.org/10.1145/351240.351266.
- Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
- Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs. CPP 2013, volume 8307 of Lecture Notes in Computer Science, pages 147-162. Springer, Cham, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_10.
- Coq development team. The Coq Proof Assistant Reference Manual, Version 8.13.2. INRIA, 2021. URL: http://coq.inria.fr.
- N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, January 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
- Catherine Dubois and Alain Giorgetti. Tests and proofs for custom data generators. Formal Aspects of Computing, 30(6):659-684, July 2018. URL: https://doi.org/10.1007/s00165-018-0459-1.
- Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: Fast, Embeddable, λProlog Interpreter. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015, volume 9450 of Lecture Notes in Computer Science, pages 460-468. Springer, Berlin, Heidelberg, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
- Katarzyna Grygiel and Pierre Lescanne. Counting and generating lambda terms. Journal of Functional Programming, 23(5):594-628, September 2013. URL: https://doi.org/10.1017/S0956796813000178.
- Leonidas Lampropoulos and Benjamin C. Pierce. QuickChick: Property-Based Testing in Coq. Software Foundations series, volume 4. Electronic textbook, August 2022. Version 1.3.1 URL: https://softwarefoundations.cis.upenn.edu/qc-1.3.1.
- Pierre Lescanne. On counting untyped lambda terms. Theoretical Computer Science, 474:80-97, February 2013. URL: https://doi.org/10.1016/j.tcs.2012.11.019.
- Nicolas Magaud. Changing data representation within the Coq system. In David A. Basin and Burkhart Wolff, editors, Theorem Proving in Higher Order Logics. TPHOLs 2003, volume 2758 of Lecture Notes in Computer Science, pages 87-102. Springer, Berlin, Heidelberg, 2003. URL: https://doi.org/10.1007/10930755_6.
- Conor McBride. Elimination with a motive. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs. TYPES 2000, volume 2277 of Lecture Notes in Computer Science, pages 197-216. Springer, Berlin, Heidelberg, 2000. URL: https://doi.org/10.1007/3-540-45842-5_13.
- Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14(1):69-111, 2004. URL: https://doi.org/10.1017/S0956796803004829.
- Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. Computing correctly with inductive relations. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pages 966-980. ACM, New York, 2022. URL: https://doi.org/10.1145/3519939.3523707.
- 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, 64(5):947-999, 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
- Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '87, pages 307-313. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41653.