# Workshop on Algebra, Geometry and Proofs in Symbolic Computation

## Overview

The focus of this workshop is on algorithms for polynomials, and their certification, having in mind the geometric study of algebraic and semi-agebraic sets and their applications.

#### Algebraic Algorithms for Polynomials

Solving systems of polynomial equations is a fundamental problem in computer algebra, with applications in many areas. In recent years, algorithms for polynomial system solving have been applied in domainsas diverse as cryptology (through attacks on several multivariate cryptosystems, computations of discrete logarithms in finite elds or on elliptic curves), statistics, the formal verification of programs and many other areas. Popular approaches include of course Grobner bases computations, but also triangular decomposition algorithms, or methods based on toric geometry for sparse systems.Recently there have been a series of improvements in both algorithms and implementation, resulting in orders of magnitude faster performance, systems which were out of far reach a few years ago being now routinely solved.

#### Computations in Real Algebraic Geometry

Real algebraic geometry mainly concerns the study of semi-algebraic sets. Computational aspects in real algebraic geometry are renewed by connections with other areas of mathematics and computer science, such as optimization, control theory robotics, computer aided geometric design, incidence theory and game theory. Recently, there has been significant progress in many problems, such as the quadratic and symmetric case, road map computation and constructive aspects in Hilbert's 17th problem. Much attention is given to certificates of positivity using Bernstein bases, or sums of squares, with connections to semi-definite programming.

#### Certified Algorithms, Computer Algebra and Proofs

Formalization of mathematics is currently a very active topic. There is progress on the foundational aspect as well as on the formalization of significant mathematical results. The impact on computer algebra is both theoretical, since constructive mathematics can help clarifying delicate algorithmic issues in computer algebra, and practical with the integration of computer algebra software and proof assistants. The impact of proof assistantson closely related areas such as computer-assisted manipulations and proofs of combinatorial identities, simplification of hypergeometric sums and more general special function expressions as well as computations in algebraic topology will be also discussed.

On-line registration is open until December 1, but also on-site during workshops. $100 registration fees; students and PDF are $50.

## Schedule

09:00 to 09:55 |
Frank Sottile, Texas A&M University |

09:55 |
Martin Helmer, University of California Berkeley |

11:10 |
Robert Krone, Queen's University |

14:40 |
Jose Rodriguez, University of Chicago |

15:55 |
Carlos D'Andrea, Universitat de Barcelona |

09:00 to 09:55 |
Pierre-Jean Spaenlehauer, INRIA |

09:55 |
Elias Tsigaridas, INRIA Paris |

11:10 |
Jean-Charles Faugere, INRIA |

14:40 |
Marc Moreno Maza |

15:55 |
Mari Emi Alonso |

09:00 to 09:55 |
Fabrice Rouillier |

09:55 |
Marie-Francoise Roy, Université de Rennes 1 |

11:10 |
Guillaume Moroz |

13:40 to 14:40 |
Mehdi Ghasemi, University of Saskatchewan |

14:40 |
Michel Coste, Universite Rennes 1 |

15:55 |
Mohab Safey El Din |

09:00 |
Greg Blekherman, Georgia Tech |

09:00 to 09:55 |
Michael Sagraloff, Max Planck Institute for Informatics |

09:55 |
Gabriela Jeronimo, Universidad de Buenos Aires |

11:10 |
Rainer Sinn |

14:40 |
Saugata Basu, Purdue University |

15:55 to 16:55 |
Cynthia Vinzant, North Carolina State University |

16:55 |
Cordian Riener, Aalto University |

09:00 to 09:55 |
Lihong Zhi, Chinese Academy of Sciences |

09:55 |
Michael Burr, Clemson University |

11:10 |
Jonathan Hauenstein, University of Notre Dame |

09:00 to 09:55 |
Thomas Hales, University of Pittsburgh |

09:55 |
James Davenport, University of Bath |

11:10 |
Francis Sergeraert, Institut Fourier |

13:45 to 14:40 |
Doron Zeilberger, Rutgers University |

14:40 |
Bruno Buchberger, Johannes Kepler University Linz |

15:55 |
Georges Gonthier, Microsoft Research |

09:00 to 09:55 |
Henri Lombardi |

09:55 |
Carsten Schneider, Johannes Kepler University Linz |

11:10 |
An exercise in formal proofs for bijective combinatorics
Assia Mahboubi, INRIA |

13:45 to 14:40 |
Christoph Koutschan, OEAW |

14:40 |
Nicolas Brisebarre, Centre national de la recherche scientifique (CNRS) and ENS Lyon |

15:55 |
Wolfgang Windsteiger, Johannes Kepler University |

09:00 to 09:55 |
Jesús Aransay |

09:55 |
Yves Bertot, INRIA |

11:10 |
Jacques Carette, McMaster University |

13:45 to 14:40 |
Cyril Cohen, INRIA |

14:40 |
William Farmer, McMaster University |