6 citations · 6 across the 9 of their papers we have counts for
9 papers
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
Yves Bertot
This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and…
Distant decimals of
Yves Bertot, Laurence Rideau, Laurent Théry
We describe how to compute very far decimals of and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where…
Formal Proofs of Transcendence for e and as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau +1
We describe the formalisation in Coq of a proof that the numbers e and are transcendental. This proof lies at the interface of two domains of mathematics that are often conside…
Formal study of plane Delaunay triangulation
Jean-François Dufourd, Yves Bertot
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulat…
Using Structural Recursion for Corecursion
Yves Bertot, Ekaterina Komendantskaya
We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition…
Inductive and Coinductive Components of Corecursive Functions in Coq
Yves Bertot, Ekaterina Komendantskaya
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for co…