[isabelle] HaTT 2016: First Call for Papers

The First International Workshop on Hammers for Type Theories
July 1, 2016, Coimbra, Portugal (co-located IJCAR 2016)

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


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,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.