Overview
HOL is the 2014 Workshop for all interested in the HOL Theorem Prover (HOL4) and its applications.
Theme
The theme of the workshop is hidden features. Though HOL4 stands behind several publications in the ITP series, many useful features and idioms lie in the minds of individual users. Furthermore, HOL4 has a long history but is under active development today. Those who have learned the system in one incarnation may not be aware of subsequent improvements.
We invite users and developers of HOL4 to expose any piece of the system, or example of its use, that they find interesting and think is mostly unknown.
A parallel theme of the workshop is feature requests, planning, and development. We solicit requests and plans for improving HOL4 from all interested people, and hope to use part of the workshop to work together on implementing and documenting features and inducting newcomers into the community.
History
This workshop can be seen as reactivating the previous HOL User Workshops, which were discontinued in 1996 when the conference series Theorem Proving in Higher-Order Logics (TPHOLs) started. TPHOLs covered theorem proving in other HOL provers. At FLoC 2010 it was further expanded to encompass all interactive theorem proving and renamed again to Interactive Theorem Proving (ITP, this workshop's host conference).