# Location and Programme

The workshop will take place on the ground floor of the Alan Turing building,

Ecole Polytechnique

route de Saclay

Palaiseau, France.

Directions can be found here.

**Program with (available) abstracts**

## Friday 8th November 2013

9:30-10:30 : Chad Brown, *Distributed Mathematics* (joint with TAFP)

10:30-11:00: Enrico Tassi, *Modelling canonical reasoning via unification hints
(Do mathematicians learn prolog at kindergarden?)*

**11:00-11:30 : Coffee break**

11:30-12:00: Ralph Matthes,
*A Coinductive Approach to Proof Search*

12:00-12:30 : Damien Pous, *Untyping Typed Algebraic Structures and Colouring Cyclic Linear Logic
Proof Nets*

12:30-13:00: Sorin Stratulat, *Certifying formula-based induction reasoning*

**13:00-14:30 : Lunch break **

14:30-15:30: David Delahaye, *Automated Deduction Modulo*

**15:30-16:00: Coffee break**

16:00-16:30: Claire Dross, *Defining new theories in SMT solvers using first-order axioms with triggers*

16:30-17:00: Damien Rouhling, *Delayed instantiation of existential variables in presence of a theory*

17:00-17:30: Arnaud Spiwack, *Implementing an interactive proof system*