HOL Workshop 2016

A workshop for anyone with an interest in the HOL theorem prover (HOL4) will be held August 25-27 2016, co-located with ITP, the 7th International Conference on Interactive Theorem Proving, at Inria Nancy - Grand Est, France.

Theme

The theme of the workshop is ProTips. We invite both expert and novice users to share tips and tactics for building efficient, maintainable, and scalable formal developments. We are especially interested to hear from the authors of new or neglected features that could aid the engineering of large proofs. We also solicit opinions from experienced users on good proof style.

A portion of the workshop will be dedicated to large examples, including CakeML, exhibiting uses or opportunities to use the protips above. We will also encourage discussion of, planning of, and hacking on improvements to HOL and its applications during the workshop.

Call for Abstracts

We request abstracts from anyone who would like to present something at the workshop, and a rough estimate of how long a slot they would like. These can be as short as 5 minutes, or up to one hour. Abstracts are due on 15 June 2016. Feedback on submissions will be returned by 1 July 2015. There will also be an opportunity for impromptu short talks at the workshop, and for discussion and hackathon as desired.

Submission Details

Submissions, and queries, can be sent by email to the workshop organiser.

History

This workshop is the third in a series started in 2014 at FLoC in Vienna. HOL workshops have a longer history spanning several decades as mentioned on the previous workshop pages.