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): * Bart Jacobs (KU Leuven, Belgium) * Georges Gonthier (Microsoft Research - Inria) 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) ------------------------------------------------------------------------------ One dashboard for servers and applications across Physical-Virtual-Cloud Widest out-of-the-box monitoring support with 50+ applications Performance metrics, stats and reports that give you Actionable Insights Deep dive visibility with transaction tracing using APM Insight. http://ad.doubleclick.net/ddm/clk/290420510;117567292;y _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
