Jul 08 2010
Séminaire Marelle : A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
On Thursday 08/07/2010, at 11h, in room Byron Blanc.
Speaker: Tuan-Minh Pham.
Title: A combination of a dynamic geometry software with a proof assistant for interactive formal proofs.
This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software, Geogebra with a proof assistant, Coq. Thanks to the features of Geogebra, users can create and manipulate geometric constructions, they discover conjectures and interactively build formal proofs with the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules verified in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Jun 30 2010
Jun 04 2010
On Friday 04/06/2010, at 11h, in room Byron Beige.
Speaker: Yves Bertot.
Title: Root isolation for one variable polynomials with rational coefficients.
Given a one variable polynomial with rational coefficients, we want to isolate its roots. In other words, we want to find a finite list of intervals such that each interval contains exactly one root of the polynomial and each root is in one of the intervals.
The approach we study is based on Bernstein coefficients. These coefficients give a discrete approximation of the behavior of a polynomial in a given closed interval. We rely on a sufficient condition concerning these coefficients (let’s call this condition C1): if the Bernstein coefficients, taken in order, have only one alternation, then the polynomial is guaranteed to have exactly one root in the corresponding interval.
The bulk of our work is to prove condition C1.
We study the relations between the coefficients and roots of a given polynomial on a given bounded interval and the coefficients and roots of the image of this polynomial after some transformations. These transformations relate the coefficients of a polynomial in the standard monomial basis to the coefficients of another polynomial in Bernstein bases. They also relate the positive roots of a polynomial to roots of the other polynomial in some bounded interval. In fact, this establishes a relation between condition C1 and Descartes’ law of sign.
May 28 2010
On Friday 28/05/2010, at 11h, in room Byron Beige.
Speaker: Ioana Pasca.
Title: Interval Analysis in Coq.
We propose a formal study of interval analysis that concentrates on theoretical aspects rather than on computational ones. In particular we are interested in conditions for regularity of interval matrices. An interval matrix is called regular if all scalar matrices included in the interval matrix have non-null determinant and it is called singular otherwise. Regularity plays a central role in solving systems of linear interval equations. Several tests for regularity are available and widely used, but sometimes rely on rather involved results, hence the interest in formally verifying such conditions of regularity. In this talk we show how we define intervals, interval matrices and operations on them in the proof assistant Coq, and verify criteria for regularity and singularity of interval matrices.
May 25 2010
On Tuesday 25/05/2010, at 11h, in room Byron Blanc.
Speaker: Thomas Hutchinson.
Title: Lesser-known OCaml Features.
In recent years the OCaml type system has been gaining new features. However, many of these additions have not been well advertised or documented. I will discuss the use of phantom types, polymorphic variants and private types. The upcoming 3.12 release of OCaml contains many new features as well. These include polymorphic recursion, first-class modules and named type parameters. I will discuss some of these forthcoming additions.
Dec 08 2009
On Tuesday 08/12/2009, at 15h30, in room Byron Blanc.
Speaker: Evgeny Makarov.
We propose a monadic higher-order language with recursion and mutable references where types can be annotated with pre- and postconditions in a manner similar to Hoare logic. Specifications in Hoare triples are written using separation logic, which allows expressing behavior of programs working with data structures stored in the heap, such as linked lists and trees, in a succinct local manner. Effect-free program terms may be freely used specifications, resulting in dependent types. We also describe an embedding in Coq and construction of a formalized proof of type safety.