2024
Safe Smooth Paths Between Straight Line Obstacles.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024
2020
Corrigendum: C floating-point proofs layered with VST and Flocq.
J. Formaliz. Reason., 2020
C floating-point proofs layered with VST and Flocq.
J. Formaliz. Reason., 2020
2018
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation.
J. Autom. Reason., 2018
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018
2017
2016
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016
2015
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials.
CoRR, 2015
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015
2014
Views of PI: Definition and computation.
J. Formaliz. Reason., 2014
2013
A Machine-Checked Proof of the Odd Order Theorem.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013
2011
A formal study of Bernstein coefficients and polynomials.
Math. Struct. Comput. Sci., 2011
A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.
Proceedings of the Computational Science and Its Applications - ICCSA 2011, 2011
2010
A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs.
Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010
Formal Study of Plane Delaunay Triangulation.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010
2009
Formal Proof of Theorems on Genetic Regulatory Networks.
Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009
2008
Inductive and Coinductive Components of Corecursive Functions in Coq.
Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, 2008
Using Structural Recursion for Corecursion.
Proceedings of the Types for Proofs and Programs, International Conference, 2008
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008
A Short Presentation of Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008
Fixed point semantics and partial recursion in Coq.
Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008
Structural Abstract Interpretation: A Formal Study Using Coq.
Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008
2007
Affine functions and series with co-inductive real numbers.
Math. Struct. Comput. Sci., 2007
Theorem proving support in programming language semantics
CoRR, 2007
2006
Extending the Calculus of Constructions with Tarski's fix-point theorem
CoRR, 2006
2005
Vérification formelle d'extractions de racines entières.
Tech. Sci. Informatiques, 2005
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.
Proceedings of the Verified Software: Theories, 2005
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005
2004
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-07964-5, 2004
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004
2003
Visualizing Geometrical Statements with GeoView.
Proceedings of the User Interfaces for Theorem Provers Workshop, 2003
Simple canonical representation of rational numbers.
Proceedings of the Mathematics, 2003
QArith: Coq Formalisation of Lazy Rational Arithmetic.
Proceedings of the Types for Proofs and Programs, International Workshop, 2003
2002
A Proof of GMP Square Root.
J. Autom. Reason., 2002
Type-Theoretic Functional Semantics.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002
2001
Formalizing Convex Hull Algorithms.
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001
Changement de représentation des structures de données en Coq: le cas des entiers naturels.
Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001
Formalizing a JVML Verifier for Initialization in a Theorem Prover.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
Changing Data Structures in Type Theory: A Study of Natural Numbers.
Proceedings of the Types for Proofs and Programs, International Workshop, 2000
Fix-Point Equations for Well-Founded Recursion in Type Theory.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000
1999
The CtCoq System: Design and Architecture.
Formal Aspects Comput., 1999
CtCoq: an environment for mathematical reasoning.
SIGSAM Bull., 1999
1998
A Generic Approach to Building User Interfaces for Theorem Provers.
J. Symb. Comput., 1998
1997
Head-Tactics Simplification.
Proceedings of the Algebraic Methodology and Software Technology, 1997
1996
CtCoq: A System Presentation.
Proceedings of the Algebraic Methodology and Software Technology, 1996
1995
Reasoning with Executable Specifications.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995
1994
Proceedings of the Theoretical Aspects of Computer Software, 1994
1992
Real theorem provers deserve real user-interfaces.
Proceedings of the 5th ACM SIGSOFT Symposium on Software Development Environments, 1992
Origin Functions in Lambda-Calculus and Term Rewriting Systems.
Proceedings of the CAAP '92, 1992
1991
Occurences in Debugger Specifications.
Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), 1991
1990
Implementation of an Interpreter for a Parallel Language in Centaur.
Proceedings of the ESOP'90, 1990