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