45 citations · 80 across the 5 of their papers we have counts for
5 papers · 1 filter
Measure Construction by Extension in Dependent Type Theory with Application to Integration
Reynald Affeldt, Cyril Cohen
We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not ye…
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
Ran Chen, Cyril Cohen, Jean-Jacques Levy +2
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 gr…
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber +1
This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent…
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano, Cyril Cohen, Maxime Dénès +2
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main…
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Assia Mahboubi, Cyril Cohen
This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers,…