| C floating-point proofs layered with VST and Flocq. | 0 | 0.34 | 2020 |
| Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. | 0 | 0.34 | 2018 |
| Distant decimals of $π$. | 0 | 0.34 | 2017 |
| Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. | 4 | 0.49 | 2016 |
| Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. | 0 | 0.34 | 2015 |
| Views Of Pi: Definition And Computation | 0 | 0.34 | 2014 |
| A machine-checked proof of the odd order theorem | 80 | 3.41 | 2013 |
| A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs | 2 | 0.38 | 2012 |
| A formal study of Bernstein coefficients and polynomials. | 6 | 0.56 | 2011 |
| A coq-based library for interactive and automated theorem proving in plane geometry | 5 | 0.53 | 2011 |
| Formal study of plane delaunay triangulation | 7 | 0.53 | 2010 |
| Formal Proof of Theorems on Genetic Regulatory Networks | 0 | 0.34 | 2009 |
| Using Structural Recursion for Corecursion | 6 | 0.62 | 2008 |
| Inductive and Coinductive Components of Corecursive Functions in Coq | 10 | 0.62 | 2008 |
| Fixed point semantics and partial recursion in Coq | 9 | 0.58 | 2008 |
| Dependently typed programming in Agda | 4 | 0.81 | 2008 |
| Canonical Big Operators | 36 | 2.08 | 2008 |
| Structural Abstract Interpretation: A Formal Study Using Coq | 6 | 0.49 | 2008 |
| Affine functions and series with co-inductive real numbers | 14 | 0.82 | 2007 |
| Theorem proving support in programming language semantics | 4 | 0.48 | 2007 |
| CoInduction in Coq | 5 | 0.53 | 2006 |
| Coq in a Hurry | 8 | 0.65 | 2006 |
| Extending the Calculus of Constructions with Tarski's fix-point theorem | 0 | 0.34 | 2006 |
| Vérification formelle d'extractions de racines entières | 0 | 0.34 | 2005 |
| Dependent Types, Theorem Proving, and Applications for a Verifying Compiler | 1 | 0.36 | 2005 |
| Filters on coinductive streams, an application to eratosthenes' sieve | 22 | 0.98 | 2005 |
| Visualizing Geometrical Statements with GeoView | 11 | 1.04 | 2004 |
| A simple canonical representation of rational numbers | 4 | 0.57 | 2003 |
| QArith: Coq Formalisation of Lazy Rational Arithmetic | 6 | 0.60 | 2003 |
| A Proof of GMP Square Root | 11 | 0.74 | 2002 |
| Type-Theoretic Functional Semantics | 5 | 0.59 | 2002 |
| Formalizing Convex Hull Algorithms | 22 | 1.25 | 2001 |
| Changement de représentation des structures de données en Coq: le cas des entiers naturels | 2 | 0.42 | 2001 |
| Formalizing a JVML Verifier for Initialization in a Theorem Prover | 15 | 1.65 | 2001 |
| Fix-Point Equations for Well-Founded Recursion in Type Theory | 24 | 1.34 | 2000 |
| Changing Data Structures in Type Theory: A Study of Natural Numbers | 7 | 0.58 | 2000 |
| The CtCoq System: Design and Architecture | 13 | 0.89 | 1999 |
| Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings | 19 | 3.84 | 1999 |
| A generic approach to building user interfaces for theorem provers | 24 | 4.10 | 1998 |
| Head-Tactics Simplification | 1 | 0.38 | 1997 |
| CtCoq: A System Presentation | 5 | 0.65 | 1996 |
| Reasoning with Executable Specifications | 13 | 1.18 | 1995 |
| Proof by Pointing | 22 | 2.32 | 1994 |
| Origin Functions in Lambda-Calculus and Term Rewriting Systems | 6 | 0.54 | 1992 |
| Implementation of an Interpreter for a Parallel Language in Centaur | 3 | 0.51 | 1990 |
