HaTT 2016 was the first workshop on Hammers for Type Theories and related tools, techniques, and experiments. The workshop took place on 1 July 2016 in Coimbra, Portugal, as an associated event of IJCAR 2016. It shared two talks with the ARQNL 2016 workshop. The EPTCS proceedings (PDF) comprise a selection of the presented papers.
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 aimed 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. More…
Important Dates
- Abstract Submission: 28 April 2016
- Full Paper Submission: 28 April 2016
- Acceptance Notification: 18 May 2016
- Camera-ready papers: 1 June 2016
- Workshop: 1 July 2016
