Document

**Published in:** LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

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.

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)

Copy BibTex To Clipboard

@InProceedings{dubois_et_al:LIPIcs.TYPES.2022.11, author = {Dubois, Catherine and Magaud, Nicolas and Giorgetti, Alain}, title = {{Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.11}, URN = {urn:nbn:de:0030-drops-184548}, doi = {10.4230/LIPIcs.TYPES.2022.11}, annote = {Keywords: Data Representations, Isomorphisms, dependent Types, formal Proofs, random Generation, lambda Terms, Coq} }

Document

**Published in:** LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore.
Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions.
In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.

Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12, author = {Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine}, title = {{A Semantics of \mathbb{K} into Dedukti}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {12:1--12:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.12}, URN = {urn:nbn:de:0030-drops-184557}, doi = {10.4230/LIPIcs.TYPES.2022.12}, annote = {Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory} }

Document

**Published in:** Dagstuhl Reports, Volume 6, Issue 10 (2017)

This report documents the program and the outcomes of Dagstuhl Seminar 16421 "Universality of Proofs" which took place October 16-21, 2016.
The seminar was motivated by the fact that it is nowadays difficult to exchange proofs from one proof assistant to another one. Thus a formal proof cannot be considered as a universal proof, reusable in different contexts. The seminar aims at providing a comprehensive overview of the existing techniques for interoperability and going further into the development of a common objective and framework for proof developments that support the communication, reuse and interoperability of proofs.
The seminar included participants coming from different fields of computer science such as logic, proof engineering, program verification, formal mathematics. It included overview talks, technical talks and breakout sessions. This report collects the abstracts of talks and summarizes the outcomes of the breakout sessions.

Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe. Universality of Proofs (Dagstuhl Seminar 16421). In Dagstuhl Reports, Volume 6, Issue 10, pp. 75-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{dowek_et_al:DagRep.6.10.75, author = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, title = {{Universality of Proofs (Dagstuhl Seminar 16421)}}, pages = {75--98}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2017}, volume = {6}, number = {10}, editor = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.10.75}, URN = {urn:nbn:de:0030-drops-69514}, doi = {10.4230/DagRep.6.10.75}, annote = {Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability} }

Document

**Published in:** LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo.

Raphaël Cauderlier and Catherine Dubois. Objects and Subtyping in the Lambda-Pi-Calculus Modulo. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 47-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cauderlier_et_al:LIPIcs.TYPES.2014.47, author = {Cauderlier, Rapha\"{e}l and Dubois, Catherine}, title = {{Objects and Subtyping in the Lambda-Pi-Calculus Modulo}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {47--71}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.47}, URN = {urn:nbn:de:0030-drops-54919}, doi = {10.4230/LIPIcs.TYPES.2014.47}, annote = {Keywords: object, calculus, encoding, dependent type, rewrite system} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail