BERTOT , Yves

We describe two approaches for the computation of mathematical constant approximations inside interactive theorem provers. These two approaches share the same basis of fixed point computation and differ only in the way the proofs of correctness of the approximations are described. The first approach performs interval computations, while the...

This course is devised as an introduction to different techniques used in studying programming language semantics. It is inspired from the first chapters of a book written in 1993 by Glynn Winskel, The formal semantics of programming languages, an introduction and published by MIT Press in the series Foundations of Computing. We will present...

This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm,...

These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1],...

No description

Dans cet article, nous donnons un exemple très simple de programmationfonctionnelle et nous montrons comment ce style de programmation seprête à des raisonnements logiques pour éviter les erreurs deprogrammation. Les raisonnements logiques peuvent eux-même êtreeffectués avec le système Coq. Cet article est également uneintroduction à...

One benefit of formal verification is the removal of design errors at early stages of complex artifacts. This is being used extensively for software with great success. We wish to extend this to domains where the distance between formal models and the real application is bigger. We choose to work on robotics. For this field, there is a large...

We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs. The tools are foundational, in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 floating-point format. Theools are modular, in that the reasoning about C programming can be done...

In the process of describing systems and their properties, users of proof assistants introduce not only recursive datatypes, but also sets constructed by a recursive process. These sets are often represented by their characteristic predicates, and we use the terms interchangeably. Such sets or predicates are said to be inductively defined and...

Nous nous intéressons à l'utilisation des systèmes de preuves basés sur la théorie des types pour l'enseignement des mathématiques. Nous voulons remettre en question l'approche répandue qui consiste à introduire d'abord les nombres naturels, puis d'autres types de nombres. Nous explorons une approche où le type des nombres réels est le seul...

We describe the formalisation in Coq of a proof that the numbers e and π are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we...

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 describe the formal verification of two theorems of theoretical biology. These theorems concern genetic regulatory networks: they give, in a discrete modeling framework, relations between the topology and the dynamics of these biological networks. In the considered discrete modeling framework, the dynamics is described by a transition graph,...

Coq is a formal system which provides both a pure, functional programminglanguage with dependent types, and an environment to write machine-checkedproofs.Using Coq, it is possible to model a system, to formalize properties this systemis expected to satisfy, and to prove the correctness of the model with respectto these properties.Coq has...

The Mathematical Components library (hereafter, MathComp) provides, among others, a number of mathematical structures organized as hierarchies. Hierarchy Builder (hereafter, HB) is an extension of the Coq proof assistant to ease the development of hierarchies of structures. MathComp 2 is the result of the port of MathComp to HB. This document...

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