

Conference Programme
Monday, November 8th 2010 
Registration (09:3010:00) 
Welcome (10:0010:15) 
Invited Talk (10:1511:15)
10:1511:15 
On the problem of computing Betti numbers of semialgebraic sets  algorithms and complexity aspects
Saugata Basu (Purdue University)
Abstract.
I will survey results on efficient algorithms for computing the Betti numbers, as as well as the EulerPoincaré characteristic, of semialgebraic sets. I will also discuss some more recent work on the connection between the problem of computing Betti numbers of semialgebraic sets and the problem of quantifier elimination in the first order theory of the reals, which leads to an analogue of the wellknown Toda's theorem in discrete complexity theory in the BlumShubSmale model.
Slides. 

Coffee Break (11:1511:45) 
11:4512:30 
Induction in Algebra: First Steps
Peter Schuster (Universitat Munich and Leeds University)
Abstract.
In algebra many a concrete statement admits a short and elegant proof by
contradiction, and using the Lemma of KuratowskiZorn. Some of these
statements have recently turned out to follow from Raoult's Open Induction
in a direct and elementary way, in which the ideal objects are eliminated.
Proofs of the latter kind may be obtained systematically from the former.
Slides.


Tutorial (12:3013:30)
12:3013:30 
Tutorial on Cylindrical Algebraic Decomposition in Coq (Part 1 of 4)
Assia Mahboubi (INRIA, Paris)
Abstract.
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, machinechecked 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
Slides.


Lunch (13:3016:00) 
Tutorial (16:0017:00)
16:0017:00 
Tutorial on Ominimal structures (Part 1 of 4)
Michel Coste (Université de Rennes)
Abstract.
I will present an introduction to ominimal 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). 0minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of ominimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univrennes1.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.
Slides.


Coffee Break (17:0017:30) 
17:3018:15 
Recursive function classes in cartesian categories
Joaquín Díaz Boils (Universidad de Valencia)
Abstract.
A progressive description will be made about which categories allow a
representation of the different classes of recursive functions by
introducing the key concepts and the main characterizations. It will
be considered the semantics of each category (cartesian with an nno,
cartesian closed with an nno, categories with finite limits,)
according to the way of its construction has been made. It will be
discussed also under what conditions one can reason by means of
equivalence relations and it will be made an introduction to a
2category classification.
Related bibliography (reduced):
P. J. Scott, Computable functions in categories, Mathematical Logic
and Theoretical Computer. Science; Proceedings of the XVI Special Year
at Maryland, 1986.
J.R.B. Cockett. On the decidability of objects in a locos en: J.W.
Gray and A. Scedrov, eds. Categories in Computer Science and Logic,
Contemporary Mathematics (American Mathematical Society, Providence,
RI, 1989).
R. Par, L. Romn, Monoidal categories with natural numbers object, Studia
Logica 48 (3) (1989) 361376.
A. Burroni, Récursivité graphique. I. Catégorie des fonctions récursives
primitives formelles, Cahiers Topologie Géom. Différentielle Catég. 27
(1) (1986)
49–79.
Noson S. Yanofsky. Towards a Definition of an Algorithm, arXiv: math/0602053v2
(2008).
R. L. Goodstein: Recursive number theory a development of recursive
arithmetic in
a logicfree equation calculus. 1957, NorthHolland Pub. Co. (Amsterdam).
Slides.


Tuesday, November 9th 2010 
Invited Talk (09:3010:30)
09:3010:30 
Persistent homology of spaces and groups
Graham Ellis (National University Ireland)
Abstract.
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 lowdimensional 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 pgroups. We'll also outline one approach to computing the persistent homology of a finite pgroup.
Slides.


10:3011:15 
Effective homology and discrete Morse theory for the computation of homology of groups
Ana Romero (Universidad de La Rioja)
Abstract.
In the talk we will present several algorithms related with the
computation of the homology
of groups, by means of different techniques of Algebraic Topology. More
concretely, we
have developed some algorithms which, making use of the effective
homology
method, construct the homology groups of EilenbergMacLane spaces K(G,1)
for
different groups G, allowing one in particular to determine the homology
groups of G.
These results can be applied to the computation of homology groups of
central extensions
and 2types. Moreover, our initial algorithms have then been improved by
means of discrete
vector fields.
Slides.


Coffee Break (11:1511:45) 
11:4512:30 
The cohomology of coherent sheaves
Mohamed Barakat (University of Kaiserslautern)
Abstract.
The category Rfpres of finitely presented modules over a computable
ring R is computable as an Abelian category in the sense that all
existential quantifiers entering the definition of Abelian categories
can be turned into constructive ones for Rfpres. This can be proved
using matrices to present the modules and to represent the module
maps. The category of coherent sheaves on an affine scheme (i.e. the
spectrum of a ring) is equivalent to the former category. The
Serrecorrespondence can be used to provide a constructive setup for
coherent sheaves over projective schemes. This correspondence can be
refined to associate to a coherent sheaf on a projective space its
total (truncated) cohomology module. This is an equivalence of
categories and a proof of computability.
Slides.


Tutorial (12:3013:30)
12:3013:30 
Tutorial on Cylindrical Algebraic Decomposition in Coq (Part 2 of 4)
Assia Mahboubi (INRIA, Paris)
Abstract.
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, machinechecked 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
Slides.


Lunch (13:3016:00) 
Tutorial (16:0017:00)
16:0017:00 
Tutorial on Ominimal structures (Part 2 of 4)
Michel Coste (Université de Rennes)
Abstract.
I will present an introduction to ominimal 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). 0minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of ominimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univrennes1.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.
Slides.


Coffee Break (17:0017:30) 
17:3018:15 
Finding positive instances of parametric polynomials
Salvador Lucas (Universidad Politécnica de Valencia)
Abstract.
Checking (semidefinite) positiveness of polynomials (more generally,
checking polynomial constraints) is essential in many practical
applications. Unfortunately, positiveness of polynomials is often
undecidable (for polynomials whose variables range over the integers)
or very costly (for polynomials over the reals). When parametric
polynomials (i.e., polynomials whose coefficients are initially
unknown) are involved in the constraints, things are even more
difficult. Parametric polynomials are often obtained when generic
solutions to verification problems are described as polynomial
constraints. In the literature, several approaches to testing
(semidefinite) positiveness of polynomials have been investigated. We
consider a number of them and explore their feasibility regarding the
problem of finding instances of parametric polynomials which can be
shown to be positive or positive semidefinite over the set of ntuples
of nonnegative real numbers.
Slides.


18:1519:00 
Gröbner Cover: An algorithm for discussing polynomial systems with parameters
Antonio Montes (Universidad Politécnica de Cataluña)
Abstract.
Gröbner bases are the computational method par excellence for studying polynomial systems. In the case of parametric polynomial systems one has to determine the reduced Gröbner basis in dependence of the values of the parameters. I will present the algorithm GröbnerCover which has as input a finite set of parametric polynomials and outputs a finite partition of the parameter space into locally closed subsets together with polynomial data, from which the reduced Gröbner basis for a given parameter point can immediately be determined. The partition of the parameter space is intrinsic and particularly simple if the system is homogeneous. Then we will see, in an application, why the exigence of such a canonical output provides rich information about the given problem.
Slides.


Wednesday, November 10th 2010 
09:0009:45 
Numerical Integration in Coq
Bas Spitters (Radboud University)
Abstract.
We report on our work to implement numerical integration (Simpson's rule) in Coq.
Slides.


09:4510:30 
Formal libraries for Algebraic Topology: status report
Jónathan Heras (Universidad de La Rioja)
Abstract.
Algebraic Topology is an abstract mathematical subject which focuses on the
study of topological spaces by algebraic means, in particular through
algebraic invariants. Techniques of Algebraic Topology can be
implemented in software systems and then used in the study of digital images;
In particular, medical images.
If we want to use these systems in real life problems, we have
to be completely sure that the systems are safe. Therefore, to increase
the reliability of these methods and the systems that implement them, we
can use Theorem Proving tools. In this talk we are going to present one
Algebraic Topology method to study digital images which has been
implemented in a software system. Moreover, the current status of the
formal libraries (deployed in the ACL2, Coq and Isabelle theorem proving
tools) related to the implemented technique is explained.
Slides.


10:3011:15 
Constructive algebra in functional programming
Anders Mörtberg (University of Gothenburg)
Abstract.
I will discuss representation of constructive algebra using functional
programming in general, and Haskell in particular. The main structure
that I have considered is the notion of coherent rings  rings in
which it is possible to solve homogeneous systems of linear equations.
Using Haskell type classes I can represent this abstractly and
implement proofs that different notion of rings are in fact coherent,
which makes it possible to solve homogeneous systems of equations over
them.
The theories that I have considered are Bézout domains, Prüfer
domains and polynomial rings. The first two of these are
nonNoetherian analogues of classical notions, namely PIDs and
Dedekind domains. By avoiding Noetherian hypotheses I get concrete
algorithms for these structures. The polynomial rings have been
implemented together with an implementation of Buchbergers algorithm
for computing Gröbner bases.
I will also be discussing recent work in formalizing the theory of
Bézout domains and GCD domains in type theory using ssreflect.
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.
Slides.


Coffee Break (11:1511:45) 
11:4512:30 
Experiments towards efficient
computations in formalized linear algebra
Maxime Dénès (INRIA)
Abstract.
Recent advances in formalization of algebra reached results of a new degree of complexity. Of late, emphasis has been put mainly on the design of such elaborate proofs, for instance through engineering of mathematical components. However, the usability of these formalisms also relies on computational capabilities, which requires new techniques. We will focus on efficiency concerns, and will discuss how native code compilation can be applied to the SSReflect framework, aiming at concretely computable descriptions of linear algebra algorithms.
Slides.


12:3013:15 
Formalising the structure of
extremal pgroups
Georges Gonthier (Microsoft Research Cambridge)
Abstract.
Extremal pgroups are the basic building blocks of Sylow theory, in which finite groups are analyzed via their psubgroups (subgroups whose order is a power of a single prime p).
Extremal pgroups, along with their close cousins the extraspecial groups, are roughly pgroups that are almost cyclic, and they arise frequently as the base case of an inductive analysis. The large body of knowledge on the structure of such groups is then brought to bear to close off the proof. Packaging this knowledge in a convenient form is a technical challenge for a computer proof library, both because of the variety of concepts involved (such as generators and relations, group functors, maximal subgroups, linear representations, and quadratic forms), and because all this knowledge is often needed at once (so splitting it up in myriads of little lemmas is not practical). We will present some of the solutions we found to these problems.
Slides.


Lunch (13:3016:00) 
Social Events/ ForMath Business Meeting (16:0020:00) 
Conference Dinner (20:30¿?:¿?) 
Thursday, November 11th 2010 
09:4510:30 
Constructive Homology Classes and Constructive Triangulations
Francis Sergeraert (Institut Fourier)
Abstract.
In Constructive Homological Algebra, an algorithm must produce,
for every "abstract" homology class, a representant cycle, that is, an
appropriate linear combination of simplices. This combination
generates a simplicial subobject.
Also, for a manifold, it is well known a triangulation produces a
generator of the highest homology group. Question: can this classical
result have a converse? Sometimes yes, at least if you are... lucky!
Using the constructive homology of P^\infty(C), we will explain how
the Kenzo program does construct triangulations of the complex
projective spaces P^n(C). In other words, in this particular case,
Kenzo is lucky.
Slides.


10:3011:15 
On the complexity of the Euler characteristic of abstract simplicial complexes. Algorithms to compute it
Eduardo Sáenz de Cabezón (Universidad de La Rioja)
Abstract.
I this talk we consider the problem of computing the Euler
characteristic of an abstract simplicial complex given its facets. First
we study the complexity of the problem and show that it is #Pcomplete.
In the second part of the talk we propose an approach to this problem
using concepts of combinatorial commutative algebra. Based on this
approach we provide two different algorithms that show good performance.
This is joint work with Bjarke Hammersholt Roune (U. Aarhus, Denmark).
Slides.


Coffee Break (11:1511:45) 
11:4512:30 
Revisiting Zariski Main Theorem from a constructive point of view
Henri Lombardi (Université de FrancheComté)
Abstract.
We explain the main steps of a constructive proof of the
Zariski Main Theorem, and discuss some applications of
this theorem in commutative algebra.
This is a join work with Thierry Coquand and MariEmi Alonso.
Slides.


Tutorial (12:3013:30)
12:3013:30 
Tutorial on Cylindrical Algebraic Decomposition in Coq (Part 3 of 4)
Assia Mahboubi (INRIA, Paris)
Abstract.
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, machinechecked 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
Slides.


Lunch (13:3016:00) 
Tutorial (16:0017:00)
16:0017:00 
Tutorial on Ominimal structures (Part 3 of 4)
Michel Coste (Université de Rennes)
Abstract.
I will present an introduction to ominimal 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). 0minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of ominimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univrennes1.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.
Slides.


Coffee Break (17:0017:30) 
17:3018:15 
Computable objects in Dmodules theory
Francisco Castro (Universidad de Sevilla)
Abstract.
Dmodules theory studies modules over the ring D of linear
differential operators. For computational purposes we can restrict
ourselves to the case of finitely generated Dmodules over the
complex Weyl algebra D=A_n.
Elements in the Weyl algebra A_n are linear differential operators
with coefficients in the polynomial ring C[x] of complex polynomials
in n variables x=(x_1,...,x_n).
The Weyl algebra A_n is (for n>0) a noncommutative noetherian ring.
For a fiven nonzero polynomial f, the ring of rational functions
C[x]_f is finitely generated considered as a module over A_n (this
main result is due to J. Bernstein). Finding a system of generators
of such a module is a computationally difficult task and it is
related to the computation of the annihilating ideal of the rational
function 1/f. This annihilating ideal can be computed by using
algorithms of T. Oaku and N. Takayama. These algorithms use Groebner
basis computations in the Weyl algebra A_n.
In this talk we will describe the role of logarithmic Dmodules in
the "logarithmic comparison conjecture", an open problem concerning
both the annihilating ideal of 1/f and the comparison between the
cohomology of the meromorphic and the logarithmic de Rham complexes
associated to the polynomial f.
Slides.


18:1519:00 
Chain calculus and Krull dimension in distributive lattices
Luis Español (Universidad de La Rioja)
Abstract.
The Krull dimension, denoted Kdim L, of a (bounded) distributive lattice L is the greatest length of nondegenerated chains of prime ideals. Finite chains of prime ideal can be represented as morphisms (cochains) P: L—> Ch(n) and, similarly, finite chains of elements in L are morphisms (chains) a: Ch(n) —> L, where Ch(n) is the standard nchain with n+2 elements including the bottom element 0 and the top element 1. We define linked chains as an equational relation between chains of the same length, and we establish some properties of this relation. Then we have a new notion of dimension which is elementary and constructive: Cdim L ≤ n if any (n+1)chain is linked. In a classical setting, a chain a belongs to a cochain P of the same length if the composition Poa is the identity on Ch(n). By using this relation the equivalence between Kdim L and Cdim L is proved. Of course, Cdim L is also equivalent to other constructive and elementary formulations of dimension proposed before now. A calculus of finite chains in L enables us to give direct proofs of these equivalences, and also to develop the theory of Cdim L. Associated to each chain a: Ch(n) —> L there are: (i) the morphism of distributive lattice l(a):L—> L(a) which is universal among the morphisms f:L—> D such that foa is contained in the center of D; (ii) the boolean sum ∫a of the elements of a. The elements of L(a) are (n+1)chains separated (to be defined) by a, and we have ∫l(a)(x)=x+∫a. A (n+1)chain x is linked if and only if there exists a nchain a such that x is complemented in L(a). This result generalizes the case n=1: a 1chain/element x in L is linked if and only if it is complemented. Etc.
Slides.


MAP Business Meeting (19:0020:00) 
Friday, November 12th 2010 
Tutorial (09:3010:30)
09:3010:30 
Tutorial on Ominimal structures (Part 4 of 4)
Michel Coste (Université de Rennes)
Abstract.
I will present an introduction to ominimal 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). 0minimal geometry is also known as "tame topology" (no monster!). Uniform finiteness in families is typical of ominimal geometry. I shall rely on an already existing set of notes available at the following address : http://perso.univrennes1.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.
Slides. 

10:3011:15 
An implementation of Abhyankar's proof of Newton theorem in Haskell
Bassel Mannaa (University of Gothenburg)
Abstract.
Newton theorem states that for a field k of zero characteristic, the algebraic closure of the field k((X)) is the union of k((X^1/m)) over all positive integers m. We present a constructive version of the theorem based on one by Abhyankar rather than the more familiar Newton polygon method. We present an implementation of the algorithm in Haskell.
Slides.


Coffee Break (11:1511:45) 
11:4512:30 
Trusted Computer Mathematics within the Focalize Environment
David Delahaye (CNAM, Paris)
Abstract.
We introduce the Focalize environment, which is an integrated development
environment designed to build certified components using theorem proving. In
Focalize, it is possible to build applications step by step, going from
abstract specifications to concrete implementations. These different structures
are combined using inheritance and parameterization, inspired by
objectoriented programming. Moreover, each of these structures is equipped
with a carrier set, providing a typical algebraic specification flavor. To
highlight these features, we present a survey of Focalize, with a complete
example of formalization in support. In addition, Focalize has been
successfully used in several significant applications, such as Computer
Algebra, and we show some excerpts from this library. Finally, Focalize comes
with a (recently rewritten) compiler producing OCaml code for execution and Coq
code for certification, as well as a firstorder automated theorem prover,
called Zenon, for the reasoning support, and we describe some examples of use.
Slides.


Tutorial (12:3013:30)
12:3013:30 
Tutorial on Cylindrical Algebraic Decomposition in Coq (Part 4 of 4)
Assia Mahboubi (INRIA, Paris)
Abstract.
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, machinechecked 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
Slides.


Lunch (13:3016:00) 
Open Session: Challenges in Formal Proofs and Mathematical Applications (16:0019:00) 
Closing Session (19:0019:30) 




