============================================= CALL FOR PAPERS The First International Workshop on Hammers for Type Theories July 1, 2016, Coimbra, Portugal (co-located IJCAR 2016) http://hatt2016.inria.fr/ =============================================
HaTT 2016 is the first workshop on Hammers for Type Theories and related tools, techniques, and experiments. HOLyHammer for HOL Light and HOL4, Sledgehammer for Isabelle/HOL, and other similar tools can have a huge impact on user productivity. These integrate automatic theorem provers (including SMT solvers) with proof assistants. However, users of proof assistants based on type theories, such as Agda, Coq, Lean, and Matita, currently miss out on this convenience. The HaTT workshop aims at gathering researchers working on these and other aspects of "hammer-style" automation for type theories, to exchange experiences and foster collaborations, to finally reach end users. Topics of interest for this workshop include all aspects of cooperation between automatic theorem provers and proof assistants based on type theory. More specifically, some suggested topics are + translation of formulas from type theory to first-order logic + translation of proofs from first-order logic to type theory + verified proof certification + lemma selection (relevance filtering) + prototypes + applications + case studies + experiments + benchmarks Researchers interested in participating are invited to submit either an extended abstract (2 to 6 pages) or a regular paper (8 to 15 pages). Submissions will be refereed by the program committee. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome, even if they describe already published work. We expect that one author of every accepted paper will present their work at the workshop. Regular papers should describe previously unpublished work and must be prepared using the LaTeX EPTCS class (see http://eptcs.org/). Papers will be submitted via EasyChair at https://easychair.org/conferences/?conf=hatt2016 Accepted regular papers will appear in an EPTCS volume. Important Dates Abstract Submission: April 4, 2016 Full Paper Submission: April 11, 2016 Acceptance Notification: May 13, 2016 Camera-ready papers: May 27, 2016 Workshop: July 1, 2016 Program Committee Jesper Bengtson (IT-Univeristy of Copenhagen) Frédéric Besson (Inria) Jasmin Christian Blanchette (Inria & MPII Saarbrücken, co-chair) Arthur Charguéraud (Inria) Claudio Sacerdoti Coen (University of Bologna) Leonardo de Moura (Microsoft Research) Jean-Christophe Filliâtre (CNRS) Liana Hadarean (Oxford University) Cătălin Hriţcu (Inria) Cezary Kaliszyk (University of Innsbruck, co-chair) Chantal Keller (Université Paris-Sud) Assia Mahboubi (Inria) Laurent Théry (Inria) Cesare Tinelli (University of Iowa) Josef Urban (Czech Technical University in Prague) -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/cek/ ------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
