6 citations · 17 across the 6 of their papers we have counts for
4 papers · 1 filter
Computable analysis and notions of continuity in Coq
Florian Steinberg, Laurent Thery, Holger Thies
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of oper…
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
Ran Chen, Cyril Cohen, Jean-Jacques Levy +2
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from gr…
Distant decimals of
Yves Bertot, Laurence Rideau, Laurent Théry
We describe how to compute very far decimals of and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where…
Formalising Sylow's theorems in Coq
Laurent Thery
This report presents a formalisation of Sylow's theorems done in {\sc Coq}. The formalisation has been done in a couple of weeks on top of Georges Gonthier's {\sc ssreflect} \cite{…