HOL4 Workshop 2015
A workshop for anyone with an interest in the HOL theorem prover (HOL4) will be held on August 2-3 2015, at CADE-25, the 25th jubilee edition of the International Conference on Automated Deduction, at Freie Universität, Berlin.
Sunday August 2nd
- Welcome and introductions. Overview (Ramana Kumar).
- Isabelle/PIDE/jEdit as integrated development environment for Standard ML (Makarius Wenzel).
- Coffee break.
- Discussion/hacking session for PIDE.
- A Hammer for HOL4 (Thibault Gauthier and Cezary Kaliszyk).
- Discussion/hacking session for Hammer.
Monday August 3rd
- Invited Talk: Defining a Niche for HOL4 (Michael Norrish).
- Discussion/hacking session for HOL4 itself.
- Theory Exploration with OpenTheory export (via HOL4) (Moa Johansson, Magnus Myreen, and Dan Rosén).
- Coffee break.
- Discussion/hacking session for HipSpec.
- HOL4 and CakeML (Magnus Myreen).
- Discussion/hacking session for CakeML.
The theme of the workshop is the development agenda. We hope to gather both users and developers of HOL4 to brainstorm and decide:
- What tasks or projects (from small to large scale) should we prioritise for HOL4's continued development?
- How can we apply the latest developments in the fields of automated and interactive theorem proving back to HOL4, and is it worth it?
- Should HOL4 merge with or evolve into another system?
- How might we increase the amount of developer time put into the system (e.g., attracting new users, holding more workshops)?
Being co-located with CADE, we also intend the workshop to be beginner-friendly with the possibility of some tutorial introductions, and we hope to focus some of the time on integrating ATP with ITP.
Finally, at the request of some potential participants, we intend to dedicate some parts of the program to the development of CakeML, a verified implementation of ML that makes heavy use of HOL4 and whose development will be affected by any major changes to HOL4.
- PIDE for HOL4
- HOL(y)Hammer integration
- Move to a kernel whose rules are proven sound
- OpenTheory upgrade to version 6; also, OpenTheory for theory storage
- Examples-driven crowdsourced documentation
- Function and datatype package extensions
- Get through some of the HOL4 issues and CakeML issues
HOL4's lead developer, Michael Norrish will speak at 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 half an hour. Abstracts are due on 15 June 2015. 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.
Submissions are to be made through EasyChair. Queries can be sent by email to the workshop organiser.
This workshop is the second in a series started last year at FLoC in Vienna. HOL workshops have a longer history spanning several decades as mentioned on last year's workshop page.