HOL4 users' workshop 2025

Tue 10th - Wed 11th June 2025

About

A workshop to bring together developers/users of the HOL4 interactive theorem prover. The hope is to:

• Learn about recent developments in HOL4.
• Discuss upcoming and planned/proposed developments in HOL4.
• Share tips and tricks, best practices, and pearls of wisdom.
• Create opportunities for collaboration and networking.

The workshop will be held at the Arm offices in Cambridge: 110 Fulbourn Rd, Cambridge CB1 9NJ, UK. In-person attendance is strongly recommended, but virtual attendance should also be possible.

Registration

Deadline: Fri 16th May (globally/Anywhere on Earth)

Please register here

List of attendees

* = virtual

• *Alex Shkotin (ACM, USA)
• *Albert Rizaldi (PlanV GmbH, Germany)
• Andreas Lööw (Imperial College London, UK)
• Daniel Nezamabadi (ETH Zurich, Switzerland and Chalmers, Sweden)
• Didrik Lundberg (KTH, Sweden and Saab AB, Sweden)
• Gergely Buday (University of Sheffield, UK)
• *Irvin Ng (Temasek Poly Student, Singapore)
• *Johannes Åman Pohjola (Chalmers, Sweden and University of Gothenburg, Sweden)
• *Konrad Slind (unaffiliated)
• Magnus Myreen (Arm, Sweden)
• Mario Carneiro (Chalmers, Sweden)
• *Michael Norrish (ANU, Australia)
• Mohammad Abdulaziz (King’s College London, UK)
• *Nikos Alexandris (Chalmers, Sweden)
• Pascal Lasnier (University of Cambridge, UK)
• Ramana Kumar (Verifereum, UK)
• Robert Söldner (University of York, UK)
• Thaïs Baudon (University of Kent, UK)
• Thibaut Pérami (University of Cambridge, UK)
• Thomas Bauereiss (University of Cambridge, UK)
• Vineet Rajani (University of Kent, UK)
• Yong Kiam Tan (NTU, Singapore)

Provisional schedule

If attending in-person, please arrive on time each day due to security restrictions. Late entry or re-entry may not be allowed. Tea, coffee, and lunch will be provided. Please do let us know if you have any dietary requirements on the registration form above.

Full schedule (with abstracts)

Please see this PDF.

Outline schedule

Tue 10th June

09:00 - 09:30	Arrival and admission
09:30 - 10:00	Lightning introductions
10:00 - 10:45	Tips + tricks: using AncestryData Michael Norrish (ANU, Australia)
10:45 - 11:15	Break
11:15 - 12:00	Discussion: documentation Led by: Anthony Fox (Arm, UK)
12:00 - 13:00	Lunch
13:00 - 13:30	GOL in GOL in HOL: using cv_compute on Conway’s Game of Life Magnus Myreen (Arm, Sweden)
13:30 - 13:45	Brack: verified compilation of Scheme to CakeML Pascal Lasnier (University of Cambridge, UK)
13:45 - 14:30	A HOL-to-ACL2 connection and Finite automata theory Konrad Slind (unaffiliated)
14:30 - 14:45	Verifereum + verified compilation for Vyper Ramana Kumar (Verifereum, UK)
14:45 - 15:15	Break
15:15 - 15:45	Towards a modern IDE experience for HOL Mario Carneiro (Chalmers, Sweden)
15:45 - 16:15	Compiling formal network semantics: lessons from CakeML and HOL4P4 Didrik Lundberg (KTH, Sweden and Saab AB, Sweden)
16:15 - 16:45	Secure compilation of the Declassification Core Calculus Thaïs Baudon (University of Kent, UK)
19:00	Dinner in central Cambridge

Wed 11th June

09:00 - 09:30	Arrival and admission
09:30 - 10:30	Discussion: UI/UX Led by: Mario Carneiro (Chalmers, Sweden)
10:30 - 11:00	Break
11:00 - 12:00	Discussion: package management Led by: Daniel Nezamabadi (ETH Zurich, Switzerland and Chalmers, Sweden)
12:00 - 13:00	Lunch
13:00 - 14:00	Discussion: the future of HOL4 development and use Led by: Ramana Kumar (Verifereum, UK)
14:00 - 14:45	Discussion: what is the next HOL platform? Led by: Konrad Slind (unaffiliated)
14:45 - 15:15	Break
15:15 - 16:15	Discussion: a guiding light for HOL4 Led by: Ramana Kumar (Verifereum, UK)
16:15 onwards	Discussion and end of day

Logistics: remote attendance

Details will be sent directly to registered participants nearer the time.

Logistics: in-person attendance

Getting to Cambridge

You can take a train to Cambridge from three main London stations: King's Cross, St. Pancras International, and Liverpool Street. Fast trains take about 50 minutes, while slower ones take up to 1.5 hours. King's Cross has the most frequent trains (about four per hour). The fastest trains operate directly from King's Cross.

Please note: there are two stations in Cambridge: Cambridge and Cambridge North. The hotels recommended below are near Cambridge, not Cambridge North.

If you are traveling from abroad, the easiest option is to fly to a London airport and take a train. London Stansted is quite close to Cambridge (and not really in London): around 40 minutes by coach or by train.

Hotels

We suggest staying near Cambridge station for ease of access. There are many hotels and AirBnB offerings in the area, for example:

• Travelodge
• ibis
• YHA youth hostel

There are many hotels/AirBnBs in central Cambridge and beyond too.

Transport to Arm

The Arm offices are in Cherry Hinton, a village a short distance from Cambridge. There are several modes of transport available between Cambridge station and the Arm offices:

• Bus: Citi 1 and Citi 3 are direct between Cambridge station and Arm (nearest stop: Limedale Close), usually every ~15 mins. During peak hours it is worth leaving ample time for traffic.
• E-scooter/e-bike: you can hire these using the Voi app.
• Taxi: Uber and so on operate in Cambridge, and you can alternatively call Panther Taxis.

Things to do in Cambridge

Cambridge is a well-known, historic university city with long-standing links to the field of computing. If you are interested in exploring it, here are a few things you could try:

• Visit central Cambridge, home to many of University of Cambridge's colleges. Highlights include:
  
  • Great St. Mary's church, whose tower has a panoramic view of central Cambridge.
  • King's College Chapel.
  • The Corpus Clock.
  • The Mathematical Bridge and the Bridge of Sighs.
  • Cambridge's many pubs, such as The Eagle (where it was announced that the structure of DNA had been discovered).
• See the River Cam, by punt (e.g. hire from Scudamore's).
• The Botanic Garden. 
• The Fitzwilliam Museum.
• The Centre for Computing History.
• Further afield (~1 hr drive), Bletchley Park codebreaking museum, the site of Alan Turing's codebreaking work during the Second World War.