THÉRY , Laurent

This note presents a formalisation done in Coq of Lucas-Lehmer test and Pocklington certificate for prime numbers. They both are direct consequences of Fermat little theorem. Fermat little theorem is proved using elementary group theory and in particular Lagrange theorem.

This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

This notes explains how the optimal algorithm for the generalised towers of Hanoi has been formalised in the Coq proof assistant using the SSReflect extension.

The Tower of Hanoi is a typical example that is used in computer science courses to illustrate all the power of recursion. In this paper, we show that it is also a very nice example for inductive proofs and formal verification. We present some non-trivial results that have been formalised in the {Coq} proof assistant.

The Tower of Hanoi is a typical example that illustrates all the power of recursion in programming. In this paper, we show that it is also a very nice example for inductive proofs and formal verification. We present some non-trivial results about it that have been formalised in the Coq proof assistant.

This notes explains how the Kosaraju's algorithm that computes the strong-connected components of a directed graph has been for-malised in the Coq prover using the SSReflect extension.

This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

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 operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on...

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 operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on...

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 1 million decimals of $π$ and the billionth hexadecimal (without the preceding ones) have been computed in a formally verified way. Three methods have been studied,...

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 operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant COQ and heavily relies on...

We present a full Coq formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers.

In order to derive efficient and robust floating-point implementations of a given function f, it is crucial to compute its hardest-to-round points, i.e. the floating-point numbers x such that f(x) is closest to the midpoint of two consecutive floating-point numbers. Depending on the floating-point format one is aiming at, this can be highly...

Comparing provers on a formalization of the same problem is always a valuable exercise. In thispaper, we present the formal proof of correctness of a non-trivial algorithm from graph theory thatwas carried out in three proof assistants: Why3,Coq, and Isabelle.

We design algorithms for the correct rounding of the power function $x^y$ in the binary64 IEEE 754 format, for all rounding modes, modulo the knowledge of hardest-to-round cases. Our implementation of these algorithms largely outperforms previous correctly-rounded implementations and is not far from the efficiency of current mathematical...

We report on the porting of the Mathematical Components library (hereafter MC) to the Hierarchy Builder [2] tool (hereafter HB).