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. Accepted regular papers will appear in an EPTCS volume.
