Yves Bertot

Available identifiers

zbMath Open bertot.yvesWikidataQ112445647 ScholiaQ112445647MaRDI QIDQ703857

List of research outcomes

Publication	Date of Publication	Type
C-language floating-point proofs layered with VST and Flocq	2021-12-02	Paper
Corrigendum: C floating-point proofs layered with VST and Flocq	2021-12-02	Paper
Views of Pi: definition and computation	2019-09-18	Paper
CtCoq: A system presentation	2019-01-15	Paper
Formal verification of a geometry algorithm: A quest for abstract views and symmetry in coq proofs	2018-11-23	Paper
Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation	2018-08-21	Paper
A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs	2014-07-22	Paper
Inductive and coinductive components of corecursive functions in Coq	2014-01-24	Paper
A Machine-Checked Proof of the Odd Order Theorem	2013-08-07	Paper
A simple canonical representation of rational numbers	2013-06-06	Paper
A formal study of Bernstein coefficients and polynomials	2011-10-21	Paper
Formal study of plane Delaunay triangulation	2010-09-14	Paper
Theorem-proving support in programming language semantics	2010-02-05	Paper
Structural Abstract Interpretation: A Formal Study Using Coq	2009-07-28	Paper
Using Structural Recursion for Corecursion	2009-07-02	Paper
A Short Presentation of Coq	2008-12-04	Paper
Canonical Big Operators	2008-12-04	Paper
Affine functions and series with co-inductive real numbers	2007-04-12	Paper
Types for Proofs and Programs	2006-11-13	Paper
Types for Proofs and Programs	2005-12-23	Paper
Typed Lambda Calculi and Applications	2005-11-11	Paper
Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.	2005-01-12	Paper
https://portal.mardi4nfdi.de/entity/Q4736398	2004-08-09	Paper
https://portal.mardi4nfdi.de/entity/Q4484334	2003-06-12	Paper
A proof of GMP square root	2003-04-27	Paper
https://portal.mardi4nfdi.de/entity/Q4790670	2003-02-04	Paper
https://portal.mardi4nfdi.de/entity/Q4551130	2002-09-04	Paper
https://portal.mardi4nfdi.de/entity/Q2754027	2001-11-11	Paper
https://portal.mardi4nfdi.de/entity/Q4490725	2000-07-20	Paper
https://portal.mardi4nfdi.de/entity/Q4871703	1996-04-02	Paper

Research outcomes over time

This page was built for person: Yves Bertot