The following pages link to Yves Bertot (Q703857):
Displayed 30 items.
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Formal verification of a geometry algorithm: A quest for abstract views and symmetry in coq proofs (Q1623113) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- A proof of GMP square root (Q1868507) (← links)
- (Q2754027) (← links)
- Inductive and Coinductive Components of Corecursive Functions in Coq (Q2873661) (← links)
- A formal study of Bernstein coefficients and polynomials (Q3094174) (← links)
- (Q3400636) (← links)
- Affine functions and series with co-inductive real numbers (Q3431543) (← links)
- A Short Presentation of Coq (Q3543643) (← links)
- Canonical Big Operators (Q3543652) (← links)
- Using Structural Recursion for Corecursion (Q3638255) (← links)
- (Q4484334) (← links)
- (Q4490725) (← links)
- (Q4551130) (← links)
- CtCoq: A system presentation (Q4647518) (← links)
- (Q4736398) (← links)
- (Q4790670) (← links)
- (Q4871703) (← links)
- A simple canonical representation of rational numbers (Q4924543) (← links)
- C-language floating-point proofs layered with VST and Flocq (Q5014364) (← links)
- Corrigendum: C floating-point proofs layered with VST and Flocq (Q5014365) (← links)
- A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs (Q5170235) (← links)
- Structural Abstract Interpretation: A Formal Study Using Coq (Q5191090) (← links)
- Views of Pi: definition and computation (Q5195256) (← links)
- A Machine-Checked Proof of the Odd Order Theorem (Q5327343) (← links)
- Typed Lambda Calculi and Applications (Q5704032) (← links)
- Types for Proofs and Programs (Q5712314) (← links)
- Formal Study of Plane Delaunay Triangulation (Q5747651) (← links)
- Types for Proofs and Programs (Q5898173) (← links)