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: 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) (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


For non IC0901 participants, registration is done through the ETAPS 2012 registration system.

Last update 20 December 2011