Automation in Proof Assistants 2012
a TYPES-affiliated satellite workshop of ETAPS 2012
organized in coordination with the Rich-Model Toolkit COST action
Sat 31 March - Sun 1 April, Tallinn, Estonia
New: Program
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
The workshop is shared on Saturday 31 March and on the morning of Sunday 1 April with
the meeting of the
COST Action IC0901
Rich-Model Toolkit
which explores how to make automated reasoning applicable to a wider
range of problems.
Invited speakers
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
(preferably) by 25 February 2012.
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.
Last update 20 December 2011