Document

**Published in:** LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature.

Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez. Machine-Checked Categorical Diagrammatic Reasoning. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guillemet_et_al:LIPIcs.FSCD.2024.7, author = {Guillemet, Beno\^{i}t and Mahboubi, Assia and Piquerez, Matthieu}, title = {{Machine-Checked Categorical Diagrammatic Reasoning}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {7:1--7:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.7}, URN = {urn:nbn:de:0030-drops-203363}, doi = {10.4230/LIPIcs.FSCD.2024.7}, annote = {Keywords: Interactive theorem proving, categories, diagrams, formal proof automation} }

Document

**Published in:** LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.

Assia Mahboubi and Matthieu Piquerez. A First Order Theory of Diagram Chasing. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{mahboubi_et_al:LIPIcs.CSL.2024.38, author = {Mahboubi, Assia and Piquerez, Matthieu}, title = {{A First Order Theory of Diagram Chasing}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {38:1--38:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.38}, URN = {urn:nbn:de:0030-drops-196817}, doi = {10.4230/LIPIcs.CSL.2024.38}, annote = {Keywords: Diagram chasing, formal proofs, abelian categories, decidability} }

Document

Invited Talk

**Published in:** LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

This talk shall discuss the potential impact of formal methods, and in particular, of interactive theorem proving, on computational mathematics.
Geared with increasingly fast computer algebra libraries and scientific computing software, computers have become amazing instruments for mathematical guesswork. In fact, computer calculations are even sometimes used to substantiate actual reasoning steps in proofs, later published in major venues of the mathematical literature. Yet surprisingly, little of the now standard techniques available today for verifying critical software (e.g., cryptographic components, airborne commands, etc.) have been applied to the programs used to produce mathematics. In this talk, we propose to discuss this state of affairs.

Assia Mahboubi. Machine-Checked Computational Mathematics (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mahboubi:LIPIcs.CALCO.2023.5, author = {Mahboubi, Assia}, title = {{Machine-Checked Computational Mathematics}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {5:1--5:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.5}, URN = {urn:nbn:de:0030-drops-188024}, doi = {10.4230/LIPIcs.CALCO.2023.5}, annote = {Keywords: Type theory, computer algebra, interactive theorem proving} }

Document

**Published in:** LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

We generalize to a rich dependent type theory a proof originally developed by Escardó that all System 𝚃 functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (ℕ → ℕ) → ℕ is externally continuous.

Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baillon_et_al:LIPIcs.CSL.2022.5, author = {Baillon, Martin and Mahboubi, Assia and P\'{e}drot, Pierre-Marie}, title = {{Gardening with the Pythia A Model of Continuity in a Dependent Setting}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {5:1--5:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.5}, URN = {urn:nbn:de:0030-drops-157256}, doi = {10.4230/LIPIcs.CSL.2022.5}, annote = {Keywords: Type theory, continuity, syntactic model} }

Document

**Published in:** LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

In this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois' Theorem of the equivalence between solvable extensions and extensions solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.

Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8, author = {Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves}, title = {{Unsolvability of the Quintic Formalized in Dependent Type Theory}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8}, URN = {urn:nbn:de:0030-drops-139038}, doi = {10.4230/LIPIcs.ITP.2021.8}, annote = {Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic} }

Document

Invited Talk

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

In this talk, we discuss the role and the implementation of mathematical structures in libraries of formalised mathematics in dependent type theory.

Assia Mahboubi. Mathematical Structures in Dependent Type Theory (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{mahboubi:LIPIcs.CSL.2021.2, author = {Mahboubi, Assia}, title = {{Mathematical Structures in Dependent Type Theory}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {2:1--2:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.2}, URN = {urn:nbn:de:0030-drops-134361}, doi = {10.4230/LIPIcs.CSL.2021.2}, annote = {Keywords: Mathematical structures, formalized mathematics, dependent type theory} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

LIPIcs, Volume 175, TYPES 2019, Complete Volume

25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{bezem_et_al:LIPIcs.TYPES.2019, title = {{LIPIcs, Volume 175, TYPES 2019, Complete Volume}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {1--256}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019}, URN = {urn:nbn:de:0030-drops-130639}, doi = {10.4230/LIPIcs.TYPES.2019}, annote = {Keywords: LIPIcs, Volume 175, TYPES 2019, Complete Volume} }

Document

Front Matter

**Published in:** LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Front Matter, Table of Contents, Preface, Conference Organization

25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2019.0, author = {Bezem, Marc and Mahboubi, Assia}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.0}, URN = {urn:nbn:de:0030-drops-130640}, doi = {10.4230/LIPIcs.TYPES.2019.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }

Document

**Published in:** LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.

Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brehard_et_al:LIPIcs.ITP.2019.8, author = {Br\'{e}hard, Florent and Mahboubi, Assia and Pous, Damien}, title = {{A Certificate-Based Approach to Formally Verified Approximations}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {8:1--8:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.8}, URN = {urn:nbn:de:0030-drops-110638}, doi = {10.4230/LIPIcs.ITP.2019.8}, annote = {Keywords: approximation theory, Chebyshev polynomials, Banach fixed-point theorem, interval arithmetic, Coq} }

Document

**Published in:** Dagstuhl Reports, Volume 8, Issue 8 (2019)

Formalized mathematics is mathematical knowledge (definitions, theorems, and proofs) represented in digital form suitable for computer processing. The central goal of this seminar was to identify the theoretical advances and practical improvements needed in the area of formalized mathematics, in order to make it a mature technology, truly useful to a larger community of students and researchers in mathematics. During the seminar, various software systems for formalization were compared, and potential improvements to existing systems were investigated. There have also been discussions on the representation of algebraic structures in formalization systems.

Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). In Dagstuhl Reports, Volume 8, Issue 8, pp. 130-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagRep.8.8.130, author = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, title = {{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}}, pages = {130--145}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2019}, volume = {8}, number = {8}, editor = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.8.130}, URN = {urn:nbn:de:0030-drops-102370}, doi = {10.4230/DagRep.8.8.130}, annote = {Keywords: formal methods, formalized mathematics, proof assistant, type theory} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

A. Tarski has shown in 1948 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore
implemented various computer algebra tools
like gcd computations, subresultant polynomial or Bernstein polynomials.

Assia Mahboubi. Programming and certifying a CAD algorithm in the Coq system. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{mahboubi:DagSemProc.05021.17, author = {Mahboubi, Assia}, title = {{Programming and certifying a CAD algorithm in the Coq system}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--18}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.17}, URN = {urn:nbn:de:0030-drops-2763}, doi = {10.4230/DagSemProc.05021.17}, annote = {Keywords: Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification.} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail