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.
Want to change the program? Write to the workshop organiser. Also see the full CADE program.


The theme of the workshop is the development agenda. We hope to gather both users and developers of HOL4 to brainstorm and decide:

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.

Development Ideas

Invited Speaker

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.

Submission Details

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.