Search Results

Documents authored by Blanqui, Frédéric

Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2024.2
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)

Authors: Frédéric Blanqui

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
There exist many proof systems, interactive or automated. However, most of them are not interoperable, which leads to an important work duplication. This is unfortunate as it slows down the formalization of more advanced mathematical results, and the democratization of proof systems in education, industry and research. This state of affairs is not just a matter of file formats. Each proof system has its own axioms and deduction rules, and those axioms and deduction rules can sometimes be incompatible. To translate a proof from one system to the other, and be able to handle so many different systems, it is important to find out a logical framework in which a logical feature used in two different systems is represented by the same construction. Research on proof system interoperability started about 30 years ago, and received some increased attention with the formalization of Hales proof of Kepler conjecture in the years 2000, because parts of this proof were initially formalized in different systems. Then, it received some new interest in the years 2010 with the increasing use of automated theorem provers in proof assistants. At about the same time appeared a new logical framework, Dedukti, which extends Edinburgh’s logical framework LF by allowing the identification of types modulo some equational theory. It has been shown that various proof systems can be nicely encoded in Dedukti, and various tools have been developed to actually represent the proofs of those systems and translate them to other systems. In this talk, I will review some of these works and tools, and present recent efforts to translate entire libraries of definitions and theorems.
Cite as

Frédéric Blanqui. Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{blanqui:LIPIcs.ITP.2024.2,
  author =	{Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Translating Libraries of Definitions and Theorems Between Proof Systems}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.2},
  URN =		{urn:nbn:de:0030-drops-207307},
  doi =		{10.4230/LIPIcs.ITP.2024.2},
  annote =	{Keywords: Logical frameworks, proof systems interoperability, type theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.19
Translating Proofs from an Impredicative Type System to a Predicative One

Authors: Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.
Cite as

Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19,
  author =	{Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar},
  title =	{{Translating Proofs from an Impredicative Type System to a Predicative One}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19},
  URN =		{urn:nbn:de:0030-drops-174801},
  doi =		{10.4230/LIPIcs.CSL.2023.19},
  annote =	{Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.24
Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity

Authors: Frédéric Blanqui

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

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.
Cite as

Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.FSCD.2022.24},
  URN =		{urn:nbn:de:0030-drops-163059},
  doi =		{10.4230/LIPIcs.FSCD.2022.24},
  annote =	{Keywords: logical framework, type theory, type universes, rewriting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.20
Some Axioms for Mathematics

Authors: Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.
Cite as

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois},
  title =	{{Some Axioms for Mathematics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20},
  URN =		{urn:nbn:de:0030-drops-142581},
  doi =		{10.4230/LIPIcs.FSCD.2021.20},
  annote =	{Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.6
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory

Authors: Gabriel Hondet and Frédéric Blanqui

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
The λΠ-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting.
Cite as

Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6,
  author =	{Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6},
  URN =		{urn:nbn:de:0030-drops-138853},
  doi =		{10.4230/LIPIcs.TYPES.2020.6},
  annote =	{Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.13
Type Safety of Rewrite Rules in Dependent Types

Authors: Frédéric Blanqui

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure that those user-defined rewriting rules preserve typing. In this paper, we give a new method to check that property using Knuth-Bendix completion.
Cite as

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{blanqui:LIPIcs.FSCD.2020.13,
  author =	{Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Type Safety of Rewrite Rules in Dependent Types}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.13},
  URN =		{urn:nbn:de:0030-drops-123353},
  doi =		{10.4230/LIPIcs.FSCD.2020.13},
  annote =	{Keywords: subject-reduction, rewriting, dependent types}
}
Document
System Description
DOI: 10.4230/LIPIcs.FSCD.2020.35
The New Rewriting Engine of Dedukti (System Description)

Authors: Gabriel Hondet and Frédéric Blanqui

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s logical framework LF where functions and type symbols can be defined by rewrite rules. It therefore contains an engine for rewriting LF terms and types according to the rewrite rules given by the user. A key component of this engine is the matching algorithm to find which rules can be fired. In this paper, we describe the class of rewrite rules supported by Dedukti and the new implementation of the matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders using higher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matching algorithm extends the technique of decision trees introduced by Luc Maranget in the OCaml compiler to this more general context.
Cite as

Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hondet_et_al:LIPIcs.FSCD.2020.35,
  author =	{Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{The New Rewriting Engine of Dedukti}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.35},
  URN =		{urn:nbn:de:0030-drops-123577},
  doi =		{10.4230/LIPIcs.FSCD.2020.35},
  annote =	{Keywords: rewriting, higher-order pattern-matching, decision trees}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.9
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Authors: Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.
Cite as

Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2019.9,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Genestier, Guillaume and Hermant, Olivier},
  title =	{{Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.9},
  URN =		{urn:nbn:de:0030-drops-105167},
  doi =		{10.4230/LIPIcs.FSCD.2019.9},
  annote =	{Keywords: termination, higher-order rewriting, dependent types, dependency pairs}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact