We describe the formalisation in Coq of a proof that the numbers `e` and `pi` 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 rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.

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 second approach relies on bounding errors, for example with the help of derivatives. As an illustration, we show how to describe good approximations of the logarithm function and we compute -- to a precision of a million decimals inside the proof system, with a guarantee that all digits up to the millionth decimal are correct. All these experiments are performed with the Coq system, but most of the steps should apply to any interactive theorem prover.

Bernstein coefficients provide a discrete approximation of the behaviour of a polynomial inside an interval. This can be used, for example, to isolate the real roots of polynomials. We prove formally a criterion for the existence of a single root in an interval and the correctness of the de Casteljau algorithm for computing Bernstein coefficients efficiently.

We propose to use the Knaster-Tarski least fixed point theorem as a basis to define recursive functions in the Calculus of Inductive Constructions. This widens the class of functions that can be modelled in type-theory based theorem proving tools to potentially nonterminating functions. This is only possible if we extend the logical framework by adding some axioms of classical logic.We claim that the extended framework makes it possible to reason about terminating or non-terminating computations and we show that extraction can also be extended to handle the new functions

We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the COQ system (Dowek et al. 1993; Bertot and Castéran 2004; Giménez 1994).

Abstract. The CtCoq user-interface is a graphical user-interface designed to be added to the Coq proof development system, acting as a broker between the human user and the logical engine. The principal design goal for CtCoq was to support large-scale proof development and we claim that this user-interface helps to increase the productivity of Coq users through powerful capabilities for elaborate mathematical notations, mouse interaction, and script management. In this paper, we review the user interface implementation to show how this design goal affects the capabilities provided by the system.

We describe formal manipulations of programming language semantics that permit execution animation for interpreters. We first study the use of occurrences in the -calculus and we describe an implementation of the notion of residuals. We then describe applications in the development of interpreters for the lazy -calculus and the parallel language Occam. 1. Introduction Formal descriptions of programming language semantics have already been shown to yield executable specifications of interpreters for these languages [Mini-ML], [Esterel]. However, while the obtained interpreters have the clear advantage of being "certified" implementations, they lack a nice user interface for the very reason that the definition only deals with semantic values. An interpreter can be tranformed into a debugging tool by adding tracing, profiling, or control of execution functionalities. For us, an execution trace is a list of basic instruction calls that describes a history of execution, a profile is a list...