[Agda] 2nd announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)

[Hugo Herbelin]

     ** Workshop on Automation in Proof Assistants 2012 **

              a satellite workshop of ETAPS 2012
   jointly organized with the Rich-Model Toolkit COST action

         Sat 31 March - Sun 1 April, Tallinn, Estonia
         http://pauillac.inria.fr/~herbelin/aipa2012

       Early registration before *** 29 January 2012 ***

Though proof assistants such as Agda, Coq, Isabelle, Matita, Mizar,
Twelf, but also ACL2, HOL-Light, HOL4, PVS and many others are
characterized as interactive theorem provers, automation is largely
present under different forms in them, and at the same time probably
not as present as what one would like. The purpose of this workshop is
to gather people working on all different aspects of automation
relevant for interactive theorem proving, starting with the following
topics:

* decision procedures on specific domains
* connecting interactive and automated theorem provers
* combination of decision procedures
* reflection techniques
* unification techniques and heuristics
* rewriting techniques and heuristics
* automatic termination checking
* program synthesis

At least the first day of the workshop (Saturday 31 March) is
organized in coordination with the COST Action IC0901 Rich-Model
Toolkit (http://richmodels.org) which explores how to make automated
reasoning applicable to a wider range of problems.

** Invited speakers **

Jean-Christophe Filliâtre (U. Paris-Sud): Why3
Jasmin Blanchette (T.U. Munich): Sledgehammer, Quickcheck, and Nitpick
Chad E. Brown (U. Saarland): Satallax

** Contributing a talk **

The workshop will be informal. In addition to invited talks, the
workshop will be based on contributed talks and discussions. To
contribute a talk, send a title and abstract to aipa2012(at)inria.fr
by ** March 5, 2012 ** (but the sooner the better).

** Post-workshop proceedings **

It is planned to edit afterward a special journal issue collecting
selected papers on the topic of the workshop.

** Program committee **

Keijo Heljanko (Aalto University, IC0901 chair)
Hugo Herbelin (INRIA Paris-Rocquencourt, AIPA chair)
Viktor Kuncak (EPFL, Lausanne)
Adam Naumowicz (University of Białystok)
Claudio Sacerdoti (University of Bologna)
Makarius Wenzel (University Paris-Sud)

** Registration **

For non IC0901 participants, registration is done through the ETAPS
2012 registration system (http://www.etaps.org/2012/registration).
Early registration deadline is: 29 January 2012.