Arm Community
Arm Community
  • Site
  • User
  • Site
  • Search
  • User
Research Collaboration and Enablement
Research Collaboration and Enablement
Research Articles HOL4 users' workshop 2025
  • Research Articles
  • Arm Research - Most active
  • Arm Research Events
  • Members
  • Mentions
  • Sub-Groups
  • Tags
  • Jump...
  • Cancel
Research Collaboration and Enablement requires membership for participation - click to join
More blogs in Research Collaboration and Enablement
  • Research Articles

Tags
  • Academics
  • Verification
  • event
Actions
  • RSS
  • More
  • Cancel
Related blog posts
Related forum threads

HOL4 users' workshop 2025

Hrutvik Kanabar
Hrutvik Kanabar
March 24, 2025
5 minute read time.

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.
Anonymous
Research Articles
  • HOL4 users' workshop 2025

    Hrutvik Kanabar
    Hrutvik Kanabar
    Tue 10th - Wed 11th June 2025. A workshop to bring together developers/users of the HOL4 interactive theorem prover.
    • March 24, 2025
  • TinyML: Ubiquitous embedded intelligence

    Becky Ellis
    Becky Ellis
    With Arm’s vast microprocessor ecosystem at its foundation, the world is entering a new era of Tiny ML. Professor Vijay Janapa Reddi walks us through this emerging field.
    • November 28, 2024
  • To the edge and beyond

    Becky Ellis
    Becky Ellis
    London South Bank University’s Electrical and Electronic Engineering department have been using Arm IP and teaching resources as core elements in their courses and student projects.
    • November 5, 2024