6 citations · 17 across the 6 of their papers we have counts for
6 papers
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…
A distributed editing environment for XML documents
Claude Pasquier, Laurent Théry
XML is based on two essential aspects: the modelization of data in a tree like structure and the separation between the information itself and the way it is displayed. XML structur…
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{…
Computer validated proofs of a toolset for adaptable arithmetic
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot +1
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dyna…