C floating-point proofs layered with VST and Flocq

Autor: Andrew W. Appel, Yves Bertot

Publikováno v: Journal of Formalized Reasoning, Vol 13, Iss 1, Pp 1-16 (2021)

We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs. The tools are foundational, in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 float

Externí odkaz: https://doaj.org/article/16ded9c99b134470a43e1808b7668c7f

Views of PI: Definition and computation

Autor: Yves Bertot, Guillaume Allais

Publikováno v: Journal of Formalized Reasoning, Vol 7, Iss 1, Pp 105-129 (2014)

We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library. In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the in

Externí odkaz: https://doaj.org/article/964a072946204bc59452a2871c0d1835

Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs

Autor: Yves Bertot

Publikováno v: Theoretical Aspects of Computing – ICTAC 2018 ISBN: 9783030025076
ICTAC
ICTAC 2018-International Colloquium on Theoretical of Computing
ICTAC 2018-International Colloquium on Theoretical of Computing, Oct 2018, Stellenbosch, South Africa

International audience; 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 triangulations are simply given as sets and th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5c61a21e25b5b9121aef0f50e2800e6f
https://doi.org/10.1007/978-3-030-02508-3_1

A Machine-Checked Proof of the Odd Order Theorem

Autor: Alexey Solovyev, Jeremy Avigad, Andrea Asperti, Georges Gonthier, Stéphane Le Roux, Sidi Ould Biha, Ioana Pasca, Assia Mahboubi, Russell O'Connor, Enrico Tassi, François Garillot, Laurence Rideau, Cyril Cohen, Laurent Théry, Yves Bertot

Publikováno v: Interactive Theorem Proving ISBN: 9783642396335
ITP
ITP 2013, 4th Conference on Interactive Theorem Proving
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩

International audience; This paper reports on a six-year collaborative effort that cul- minated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8edf5c2f030660500c9cd44d945cff0e
http://hdl.handle.net/11585/185912

Interactive Theorem Proving and Program Development : Coq’Art: The Calculus of Inductive Constructions

Autor: Yves Bertot, Pierre Castéran

Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic intro