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
https://portal.mardi4nfdi.de/entity/Q3400636	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Yves Bertot