[TYPES/announce] HaTT 2016: First Call for Papers

[Cezary Kaliszyk]

=============================================
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/