Search Results

Documents authored by Mahboubi, Assia

Document
DOI: 10.4230/LIPIcs.FSCD.2024.7
Machine-Checked Categorical Diagrammatic Reasoning

Authors: Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez

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

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

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
DOI: 10.4230/LIPIcs.CSL.2024.38
A First Order Theory of Diagram Chasing

Authors: Assia Mahboubi and Matthieu Piquerez

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

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

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
DOI: 10.4230/LIPIcs.CALCO.2023.5
Machine-Checked Computational Mathematics (Invited Talk)

Authors: Assia Mahboubi

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

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

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
DOI: 10.4230/LIPIcs.CSL.2022.5
Gardening with the Pythia A Model of Continuity in a Dependent Setting

Authors: Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot

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

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

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
DOI: 10.4230/LIPIcs.ITP.2021.8
Unsolvability of the Quintic Formalized in Dependent Type Theory

Authors: Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub

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

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

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
DOI: 10.4230/LIPIcs.CSL.2021.2
Mathematical Structures in Dependent Type Theory (Invited Talk)

Authors: Assia Mahboubi

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

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

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
DOI: 10.4230/LIPIcs.TYPES.2019
LIPIcs, Volume 175, TYPES 2019, Complete Volume

Authors: Marc Bezem and Assia Mahboubi

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

Abstract
LIPIcs, Volume 175, TYPES 2019, Complete Volume
Cite as

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
DOI: 10.4230/LIPIcs.TYPES.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Marc Bezem and Assia Mahboubi

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

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
DOI: 10.4230/LIPIcs.ITP.2019.8
A Certificate-Based Approach to Formally Verified Approximations

Authors: Florent Bréhard, Assia Mahboubi, and Damien Pous

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

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

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
DOI: 10.4230/DagRep.8.8.130
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)

Authors: Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi

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

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

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
DOI: 10.4230/DagSemProc.05021.17
Programming and certifying a CAD algorithm in the Coq system

Authors: Assia Mahboubi

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

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

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.}
}
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