I will survey results on efficient algorithms for computing the Betti numbers, as as well as the Euler-Poincaré characteristic, of semi-algebraic sets. I will also discuss some more recent work on the connection between the problem of computing Betti numbers of semi-algebraic sets and the problem of quantifier elimination in the first order theory of the reals, which leads to an analogue of the well-known Toda's theorem in discrete complexity theory in the Blum-Shub-Smale model.

This tutorial presents an ongoing work on the formal proof on correctness of the Cylindrical Algebraic Decomposition Algorithm in the Coq system. The Coq system is a proof assistant based on type theory which provides a framework to implement algorithms, state theorems, and develop formal, machine-checked proofs of these theorems. It is also possible to evaluate programs efficiently inside Coq.

The Cylindrical Algebraic Decomposition Algorithm (CAD), proposed by Collins in 1973, is a complete quantifier elimination procedure for real closed fields, hence in particular for the field of real numbers.

Programming and certifying this algorithm in a proof assistant is a way to provide an automated and formal proof producing decision procedure for the first order theory of real numbers. Such automation would be of great help to relieve the user from tedious proofs of technical lemmas.

Such formal proof of correctness is also a challenging formalisation, since it relies on non trivial results of real algebraic geometry.

The tutorial will give an overview of the CAD algorithm and of its implementation, and will review the salient issues of the ongoing formalisation, without assuming specific knowledge about the Coq system.

This work has been partially funded by the FORMATH project, nr. 243847, of the FET program within the 7th Framework program of the European Commission

I will present an introduction to o-minimal geometry. This is a framework in which most of the nice features of semialgebraic or subanalytic geometry are present; it encompasses several other interesting examples (such as the exponential function). 0-minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of o-minimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univ-rennes1.fr/michel.coste/polyens/OMIN.pdf. I shall try to put emphasis on aspects related to finiteness, complexity and uniformity and to include recent developements not mentioned in the notes.

We'll begin with a brief introduction to some fairly recent work of Gunnar Carlsson, Herbert Edelsbrunner and others which uses the efficient computation of low-dimensional homology of spaces as an effective technique for investigating large data sets arising in applied problems from biology and physics. Their work is based on the notion of a persistent homology module. We'll then explain how the notion of persistent homology can also be applied to group homology. It provides a strong group invariant and we'll suggest that it might be of use in the coclass study of finite p-groups. We'll also outline one approach to computing the persistent homology of a finite p-group.

This tutorial presents an ongoing work on the formal proof on correctness of the Cylindrical Algebraic Decomposition Algorithm in the Coq system. The Coq system is a proof assistant based on type theory which provides a framework to implement algorithms, state theorems, and develop formal, machine-checked proofs of these theorems. It is also possible to evaluate programs efficiently inside Coq.

The Cylindrical Algebraic Decomposition Algorithm (CAD), proposed by Collins in 1973, is a complete quantifier elimination procedure for real closed fields, hence in particular for the field of real numbers.

Programming and certifying this algorithm in a proof assistant is a way to provide an automated and formal proof producing decision procedure for the first order theory of real numbers. Such automation would be of great help to relieve the user from tedious proofs of technical lemmas.

Such formal proof of correctness is also a challenging formalisation, since it relies on non trivial results of real algebraic geometry.

The tutorial will give an overview of the CAD algorithm and of its implementation, and will review the salient issues of the ongoing formalisation, without assuming specific knowledge about the Coq system.

This work has been partially funded by the FORMATH project, nr. 243847, of the FET program within the 7th Framework program of the European Commission

I will present an introduction to o-minimal geometry. This is a framework in which most of the nice features of semialgebraic or subanalytic geometry are present; it encompasses several other interesting examples (such as the exponential function). 0-minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of o-minimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univ-rennes1.fr/michel.coste/polyens/OMIN.pdf. I shall try to put emphasis on aspects related to finiteness, complexity and uniformity and to include recent developements not mentioned in the notes.

This tutorial presents an ongoing work on the formal proof on correctness of the Cylindrical Algebraic Decomposition Algorithm in the Coq system. The Coq system is a proof assistant based on type theory which provides a framework to implement algorithms, state theorems, and develop formal, machine-checked proofs of these theorems. It is also possible to evaluate programs efficiently inside Coq.

The Cylindrical Algebraic Decomposition Algorithm (CAD), proposed by Collins in 1973, is a complete quantifier elimination procedure for real closed fields, hence in particular for the field of real numbers.

Programming and certifying this algorithm in a proof assistant is a way to provide an automated and formal proof producing decision procedure for the first order theory of real numbers. Such automation would be of great help to relieve the user from tedious proofs of technical lemmas.

Such formal proof of correctness is also a challenging formalisation, since it relies on non trivial results of real algebraic geometry.

The tutorial will give an overview of the CAD algorithm and of its implementation, and will review the salient issues of the ongoing formalisation, without assuming specific knowledge about the Coq system.

This work has been partially funded by the FORMATH project, nr. 243847, of the FET program within the 7th Framework program of the European Commission

I will present an introduction to o-minimal geometry. This is a framework in which most of the nice features of semialgebraic or subanalytic geometry are present; it encompasses several other interesting examples (such as the exponential function). 0-minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of o-minimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univ-rennes1.fr/michel.coste/polyens/OMIN.pdf. I shall try to put emphasis on aspects related to finiteness, complexity and uniformity and to include recent developements not mentioned in the notes.

I will present an introduction to o-minimal geometry. This is a framework in which most of the nice features of semialgebraic or subanalytic geometry are present; it encompasses several other interesting examples (such as the exponential function). 0-minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of o-minimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univ-rennes1.fr/michel.coste/polyens/OMIN.pdf. I shall try to put emphasis on aspects related to finiteness, complexity and uniformity and to include recent developements not mentioned in the notes.

This tutorial presents an ongoing work on the formal proof on correctness of the Cylindrical Algebraic Decomposition Algorithm in the Coq system. The Coq system is a proof assistant based on type theory which provides a framework to implement algorithms, state theorems, and develop formal, machine-checked proofs of these theorems. It is also possible to evaluate programs efficiently inside Coq.

The Cylindrical Algebraic Decomposition Algorithm (CAD), proposed by Collins in 1973, is a complete quantifier elimination procedure for real closed fields, hence in particular for the field of real numbers.

Programming and certifying this algorithm in a proof assistant is a way to provide an automated and formal proof producing decision procedure for the first order theory of real numbers. Such automation would be of great help to relieve the user from tedious proofs of technical lemmas.

Such formal proof of correctness is also a challenging formalisation, since it relies on non trivial results of real algebraic geometry.

The tutorial will give an overview of the CAD algorithm and of its implementation, and will review the salient issues of the ongoing formalisation, without assuming specific knowledge about the Coq system.

This work has been partially funded by the FORMATH project, nr. 243847, of the FET program within the 7th Framework program of the European Commission