[Agda] Hammers for Type Theories: Second Call for Papers

[Jasmin Blanchette]

HaTT 2016: Call for Papers

The First International Workshop on Hammers for Type Theories
1 July 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 (tentatively): July 1, 2016


Program Committee

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 (The University of Iowa)
Josef Urban (Czech Technical University in Prague)