From: Tjark Weber <tjark.weber@it.uu.se>
Workshop ATP meets ITP (AMI 2015)
August 2, 2015, Berlin, Germany
affiliated with CADE 25
Aims and scope: The AMI workshop provides an informal platform for
researchers interested in automated theorem proving (ATP) and
interactive theorem proving (ITP), for instance, developers and users
of ATP, SMT and similar systems, and developers and users of ITP
systems such as Coq, HOL, Isabelle or Mizar. Its aim is the exchange
of experiences and ideas for pushing these technologies further into
the mainstream: to explore methods or tools from ATP that could be
benefit ITP and vice versa; to advance the integration and convergence
of these technologies, e.g., by considering tools and techniques from
mathematics, programming languages or AI; to bring ATP and ITP work
flows closer to mathematical and engineering practice.
Workshop topics include
proof automation for ITP: from tactics and decision procedures
via FOL to fragments of CoC and HOL; ATP with types and data types;
ATP with large data sets (as generated by ITP systems): machine
learning and other AI approaches, proof management;
theory hierarchies in ITP/ATP systems: their design and management;
ideas and techniques from mathematics and programming;
use and user experience: ATP/ITP uses and integrations in fields
like formalised mathematics or hardware/software verification.
Invited speakers (joint with the PxTP workshop):
Submissions: To foster discussions, we ask for submissions of extended
abstracts of 2 to 4 pages as well as for full papers of at most 15
pages. If submissons are based on previously published material that
should be stated clearly. Presentations will be selected based on the
quality of their contribution and their relevance to the workshop.
All accepted submissions will be published online at the workshop web
site. Quality of submissions permitting, we are planning their
considation for a journal special issue after the workshop. Papers
must be submitted via EasyChair.
Important dates:
Abstract submission: May 15, 2015 (extended)
Paper submission: May 22, 2015 (extended)
Notification: June 16, 2015
Final Version: June 25, 2015
Workshop: August 2, 2015
Program committee:
Christoph Benzmüller
Nicolai Bjørner
Simon Foster
Mike Gordon
Tim Griffin
Sebastiaan Joosten
Chantal Keller
Gerwin Klein
Assia Mahboubi
Andrei Paskevich
Stephan Schulz
Organisers:
Damien Pous (ENS Lyon, France)
Georg Struth (University of Sheffield, UK)
Tjark Weber (Uppsala University, Sweden)
Last updated: Nov 21 2024 at 12:39 UTC