HOL4 Workshop 2014

A workshop for anyone with an interest in the HOL theorem prover (HOL4) will be held on July 13th, 2014, at FLoC 2014, in association with ITP, as part of the Vienna Summer of Logic.

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.

Program

See the workshop page on the VSL 2014 website for a link to the program.

The workshop will be geared towards demonstrations, hacking, and discussion, interspersed in a program of invited speakers. It may be run in a somewhat “unconference” style to maximize the usefulness to all participants, and to encourage people to show off what they know.

Call for Abstracts

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).