Search Results

Documents authored by Cohen, Cyril

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
System Description
DOI: 10.4230/LIPIcs.FSCD.2020.34
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)

Authors: Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi

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

Abstract
It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized. Still, building algebraic hierarchies in a proof assistant such as Coq requires a lot of manual labor and often a deep expertise in the internals of the prover. Moreover, according to our experience, making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this paper we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure backward compatibility. We implement the HB language in the hierarchy-builder addon for the Coq system using the Elpi extension language.
Cite as

Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.FSCD.2020.34,
  author =	{Cohen, Cyril and Sakaguchi, Kazuhiko and Tassi, Enrico},
  title =	{{Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{34:1--34:21},
  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.34},
  URN =		{urn:nbn:de:0030-drops-123562},
  doi =		{10.4230/LIPIcs.FSCD.2020.34},
  annote =	{Keywords: Algebraic Hierarchy, Packed Classes, Coq, Elpi, Metaprogramming, \lambdaProlog}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.13
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

Authors: Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry

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

Abstract
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.
Cite as

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2019.13,
  author =	{Chen, Ran and Cohen, Cyril and L\'{e}vy, Jean-Jacques and Merz, Stephan and Th\'{e}ry, Laurent},
  title =	{{Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{13:1--13: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.13},
  URN =		{urn:nbn:de:0030-drops-110683},
  doi =		{10.4230/LIPIcs.ITP.2019.13},
  annote =	{Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.5
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Authors: Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
Cite as

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5,
  author =	{Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  title =	{{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{5:1--5:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5},
  URN =		{urn:nbn:de:0030-drops-84754},
  doi =		{10.4230/LIPIcs.TYPES.2015.5},
  annote =	{Keywords: univalence axiom, dependent type theory, cubical sets}
}
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