Main Speakers:
- Michel Coste, Université de Rennes : Tutorial on O-minimal structures.
- 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.
- Assia Mahboubi, INRIA, Paris: Tutorial on Cylindrical Algebraic Decomposition in Coq.
- 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
- Saugata Basu, Purdue University: On the problem of computing Betti numbers of semi-algebraic sets -- algorithms and complexity aspects.
- 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.
- Graham Ellis, National University of Ireland :
Persistent homology of spaces and groups.
- 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.
Scientific Committee:
- Thierry Coquand,
- Marie Françoise Roy,
- Henri Lombardi,
- Julio Rubio
Organizers:
- Luis Español,
- Julio Rubio
Local Organizing Committee:
