Workshop for HOL4 users

Tue 25th - Wed 26th June 2024

About

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

• Understand the landscape of current HOL4 usage by hosting presentations.
• Learn about recent and upcoming developments in HOL4.
• Share tips and tricks, best practices, and pearls of wisdom.
• Create opportunities for collaboration and networking/recruitment.

Michael Norrish, the primary developer of HOL4, will be delivering an invited talk.

The workshop will be held at the Arm offices in Cambridge, UK: 110 Fulbourn Rd, Cambridge CB1 9NJ

Call for participation

We are keeping the format and length deliberately open.

Register here to attend!

There is space for you indicate in the registration form whether you would like to share anything at the workshop - please do consider showing something! We're keeping the format deliberately non-prescriptive, but some suggested starting points are:

• Length: 5 mins - 45 mins
• Format: traditional presentation, demonstration, tutorial, screen-share, standing at a whiteboard, ...
• Content: technical talk, proof pearl, cool feature/automation, neat tip/trick/editor setup, work-in-progress, future/proposed line of work, ...

Proceedings

Available here.

List of attendees

• Alex Joseph Coleman (University of Kent, UK)
• Andreas Lindner (KTH, Sweden)
• Andreas Lööw (Imperial College London, UK)
• Anthony Fox (Arm)
• Anoud Alshnakat (KTH, Sweden)
• Didrik Lundberg (KTH, Sweden)
• Eleni Vafeiadi Bila (Arm)
• Henrik Akira Karlsson (KTH, Sweden)
• Hrutvik Kanabar (Arm)
• Hugo Vincent (Arm)
• Jade Alglave (Arm) (+ Hadrien Renaud, Nikos Nikoleris, Roman Manevich)
• Magnus Myreen (Arm)
• Michael Norrish (ANU, Australia)
• Milad Ketabi (University of Surrey, UK)
• Ramana Kumar (unaffiliated)
• Robert Soeldner (University of York, UK)
• Roberto Guanciale (KTH, Sweden)
• Shale Xiong (Arm)
• Thibaut Pérami (University of Cambridge, UK)
• Thomas Bauereiss (University of Cambridge, UK)
• Yong Kiam Tan (unaffiliated)

Schedule

Due to security restrictions at Arm, please arrive promptly each day. It will be difficult to allow late entry (or re-entry should you leave the building).

Tea, coffee, and lunch will be provided. Please do let us know if you have any dietary requirements.

Tue 25th June

Wed 26th June

Logistics

Getting to Cambridge

Cambridge is accessible by train from three main London stations: King's Cross, St. Pancras International, and Liverpool Street. There are a mixture of fast (~50 mins) and slow (<1.5 hr) trains, most frequently from King's Cross (~4 per hour). The fastest trains operate directly from King's Cross.

NB there are two stations in Cambridge: "Cambridge" and "Cambridge North". The first one (i.e. just "Cambridge") is the "main" one.

For those travelling from abroad, flying to a London airport and then taking a train is usually easiest. London Stansted in particular 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.