Yves Bertot - RankMe

64 papers A* 2A 2B 7C 2Misc 1Journal 23Unranked 25

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	Formally Verifying a Vertical Cell Decomposition Algorithm. ITP Yves Bertot, Thomas Portet
2024	B	`ed.`	15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, September 9-14, 2024 ITP Yves Bertot, Temur Kutsia, Michael Norrish
2024	—	`conf`	Safe Smooth Paths Between Straight Line Obstacles. Logics and Type Systems in Theory and Practice Yves Bertot
2020	J	`jnl`	C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. Andrew W. Appel, Yves Bertot
2020	J	`jnl`	Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. Andrew W. Appel, Yves Bertot
2018	J	`jnl`	Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reason. Yves Bertot, Laurence Rideau, Laurent Théry
2018	C	`conf`	Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. ICTAC Yves Bertot
2018	J	`jnl`	Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. CoRR Yves Bertot
2017	J	`jnl`	Distant decimals of $π$. CoRR Yves Bertot, Laurence Rideau, Laurent Théry
2017	B	`ed.`	Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 CPP Yves Bertot, Viktor Vafeiadis
2016	B	`conf`	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. CPP Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
2015	B	`conf`	Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. CPP Yves Bertot
2015	J	`jnl`	Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. CoRR Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
2014	J	`jnl`	Views of PI: Definition and computation. J. Formaliz. Reason. Yves Bertot, Guillaume Allais
2013	B	`conf`	A Machine-Checked Proof of the Odd Order Theorem. ITP Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
2011	—	`conf`	A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. ICCSA (4) Tuan-Minh Pham, Yves Bertot, Julien Narboux
2011	J	`jnl`	A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. Yves Bertot, Frédérique Guilhot, Assia Mahboubi
2010	—	`conf`	A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. UITP Tuan-Minh Pham, Yves Bertot
2010	B	`conf`	Formal Study of Plane Delaunay Triangulation. ITP Jean-François Dufourd, Yves Bertot
2010	J	`jnl`	Formal study of plane Delaunay triangulation CoRR Jean-François Dufourd, Yves Bertot
2009	Misc	`conf`	Formal Proof of Theorems on Genetic Regulatory Networks. SYNASC Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard
2009	J	`jnl`	Using Structural Recursion for Corecursion CoRR Yves Bertot, Ekaterina Komendantskaya
2008	—	`conf`	A Short Presentation of Coq. TPHOLs Yves Bertot
2008	—	`conf`	Canonical Big Operators. TPHOLs Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
2008	C	`conf`	Fixed point semantics and partial recursion in Coq. PPDP Yves Bertot, Vladimir Komendantsky
2008	J	`jnl`	Inductive and Coinductive Components of Corecursive Functions in Coq CoRR Yves Bertot, Ekaterina Komendantskaya
2008	—	`conf`	Inductive and Coinductive Components of Corecursive Functions in Coq. CMCS Yves Bertot, Ekaterina Komendantskaya
2008	—	`conf`	Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School Yves Bertot
2008	J	`jnl`	Structural abstract interpretation, A formal study using Coq CoRR Yves Bertot
2008	—	`conf`	Using Structural Recursion for Corecursion. TYPES Yves Bertot, Ekaterina Komendantskaya
2007	J	`jnl`	Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. Yves Bertot
2007	J	`jnl`	Theorem proving support in programming language semantics CoRR Yves Bertot
2006	J	`jnl`	Affine functions and series with co-inductive real numbers CoRR Yves Bertot
2006	J	`jnl`	CoInduction in Coq CoRR Yves Bertot
2006	J	`jnl`	Coq in a Hurry CoRR Yves Bertot
2006	J	`jnl`	Extending the Calculus of Constructions with Tarski's fix-point theorem CoRR Yves Bertot
2005	—	`conf`	Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE Yves Bertot, Laurent Théry
2005	—	`conf`	Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA Yves Bertot
2005	J	`jnl`	Vérification formelle d'extractions de racines entières. Tech. Sci. Informatiques Yves Bertot
2004	—	`conf`	A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES Yves Bertot, Benjamin Grégoire, Xavier Leroy
2004	—	`book`	Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions Yves Bertot, Pierre Castéran
2003	—	`conf`	QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES Milad Niqui, Yves Bertot
2003	—	`conf`	Simple canonical representation of rational numbers. Mathematics, Logic and Computation @ ICALP Yves Bertot
2003	—	`conf`	Visualizing Geometrical Statements with GeoView. UITP@TPHOLs Yves Bertot, Frédérique Guilhot, Loic Pottier
2002	J	`jnl`	A Proof of GMP Square Root. J. Autom. Reason. Yves Bertot, Nicolas Magaud, Paul Zimmermann
2002	—	`conf`	Type-Theoretic Functional Semantics. TPHOLs Yves Bertot, Venanzio Capretta, Kuntal Das Barman
2001	—	`conf`	Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA Nicolas Magaud, Yves Bertot
2001	—	`conf`	Formalizing Convex Hull Algorithms. TPHOLs David Pichardie, Yves Bertot
2001	A*	`conf`	Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV Yves Bertot
2000	—	`conf`	Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES Nicolas Magaud, Yves Bertot
2000	—	`conf`	Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs Antonia Balaa, Yves Bertot
1999	J	`jnl`	CtCoq: an environment for mathematical reasoning. SIGSAM Bull. Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry
1999	J	`jnl`	The CtCoq System: Design and Architecture. Formal Aspects Comput. Yves Bertot
1999	—	`ed.`	Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings TPHOLs Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry
1998	J	`jnl`	A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. Yves Bertot, Laurent Théry
1997	—	`conf`	Head-Tactics Simplification. AMAST Yves Bertot
1996	—	`conf`	CtCoq: A System Presentation. AMAST Janet Bertot, Yves Bertot
1996	A	`conf`	CtCoq: A System Presentation. CADE Janet Bertot, Yves Bertot
1995	—	`conf`	Reasoning with Executable Specifications. TAPSOFT Yves Bertot, Ranan Fraer
1994	—	`conf`	Proof by Pointing. TACS Yves Bertot, Gilles Kahn, Laurent Théry
1992	—	`conf`	Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP Yves Bertot
1992	—	`conf`	Real theorem provers deserve real user-interfaces. SDE Laurent Théry, Yves Bertot, Gilles Kahn
1991	A*	`conf`	Occurences in Debugger Specifications. PLDI Yves Bertot
1990	A	`conf`	Implementation of an Interpreter for a Parallel Language in Centaur. ESOP Yves Bertot