Proof Systems for Mathematics and Verification

, EPFL, Lausanne (see some views from above)

A joint 2024 meeting of:


Promote and compare proof systems in formal verification, logic, and mathematics, motivated by the potential for collaboration between formal methods in computer science, collaborative formal mathematics, and AI.

Date: June 14 and 15, 2024

This was primarily an in-person meeting with talks and breaks for discussions, with additional remote participation via the Zoom links. Several talk recordings are available via clicking on the talk title.

Program for Friday, June 14

Zoom Link for Friday

Time Speaker
09:15 Welcome Coffee in BCH 2201
09:50 Opening
10:00 Assia Mahboubi Proof transfer for free, beyond type equivalence
11:00 Jeremy Avigad Mathematical Structures in Dependent Type Theory (slides)
12:15 Lunch ("Native", More)
13:30 Shortest path back (in Must-See-Rolex-Learning-Center Metric)
14:00 Chelsea Edmonds Formal Probabilistic Techniques for Combinatorics in Isabelle/HOL (video starts at slide 11 due to a recording error; for the beginning see the slide deck)
15:00 Natarajan Shankar Beautiful Formalizations and Proofs (abstract)
16:00 Coffee
16:30 Jasmin Blanchette Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL
17:30 John Harrison Theorem proving infrastructure for verified cryptography (abstract)
18:30 Informal Discussion
19:00 Amphitheater Closes

Program for Saturday, June 15

Zoom Link for Saturday

Time Speaker
09:00 Lutz Straßburger What is combinatorial proof theory?
09:30 Philipp Ruemmer A proof system for reasoning about string constraints (and its formalization) (slides)
10:00 Carsten Fuhs Proving Equivalence of Imperative Programs via Constrained Rewriting Induction (slides)
10:30 Coffee
11:00 Geoff Sutcliffe The TPTP Formats for Proofs and Models (our new homepage)
11:30 Mathias Fleury and Bruno Andreotti Alethe, A flexible proof format with fine-grained steps (audio is from minute 8 only, but see the slides)
12:00 Lunch (restaurant or burgers)
14:00 Julian Parsert Guiding Function Synthesis with AI (slides)
14:30 Roussanka Loukanova Semantics of Propositional Attitudes in Type-Theory of Algorithms (slides)
15:00 Final discussions over coffee


EPFL Campus in Lausanne, walking distance from the SwissTech hotel on the EPFL metro stop of M1 metro (closest M1 stop to event location is "UNIL Sorge"). The EPFL metro stop is 15 minutes from the Lausanne train station, which has direct trains from Geneva and Zurich airports and a TGV from Paris.

Click to see:

EPFL Campus Aerial View

International Participants (Partial List)

Bruno Andreotti UFMG, Brasil
Jeremy Avigad CMU, USA
Jasmin Blanchette LMU, Germany
Adrien Champion France
Chelsea L Edmonds Sheffield, UK
Mathias Fleury Freiburg, Germany
Carsten Fuhs Birkbeck, UK
John Harrison (zoom) AWS, USA
Laurentiu Leustean (zoom) Bucharest, Romania
Roussanka Loukanova BAS, Bulgaria
Assia Mahboubi INRIA, France
Fatih Özkaynak Fırat, Turkey
Julian Parsert Innsbruck, Austria
Philipp Rümmer Regensburg, Germany
Amar Shah Berkeley, USA
Natarajan Shankar SRI, USA
Alexander Steen (zoom) Greifswald, Germany
George Metcalfe Bern, Switzerland
Lutz Straßburger Polytechnique, France
Manuela Busaniche UNL, Argentina
Samuel Gruetter MIT, USA
Bruno Andreotti UFMG, Brazil
Geoff Sutcliffe University of Miami, USA


Participants from Switzerland

Aurèle Barrière, Prof. Thomas Bourgeat (now at EPFL), Matthieu Bovel, Mario Bucev, Can Cebeci, Samuel Chassot, Shardul Chiplunkar, Basil Contovounesios, Arnaud Daby-Seesaral, Armand Feuilleaubois, Shabnam Ghasemirad, Yawen Guan, Simon Guilloud, Tao Lyu, Prof. George Metcalfe, Dragana Milovancevic, Borja Sierra Miranda, Alexandre Pinazza, Beatrice Pitton, Auguste Poiroux, Hao Sun, Prof. Maryna Viazovska (wikipedia page), Dominik Winterer, Marcin Wojnarowski, Chengyu Zhang

Hotels and Local Transit

On EPFL campus:

There are many hotels in Lausanne, including places such as "ibis Styles Lausanne Center MadHouse" in the lively and easy-to-reach Flon area of Lausanne. For apartment accommodation some of the VisionApartments buildings can be a good choice. Booking early will generally give better prices.

Hotels provide a free local public transportation card valid for metro and bus. Please consult the transportation search web site. Here is how to get from the Lausanne train station to EPFL:

EuroProofNet Travel Support

If you are a member of EuroProofNet European Research Network (COST Action), you may apply for travel support to attend the meeting. Local organizers are not responsible for COST funding decisions or procedures, but we will do our best to help. To do so, you need to register above using the Google form and indicate you will apply for the COST funding. Please keep in mind the following if you apply for funding:

  1. the reimbursement rules of EuroProofNet apply
  2. to obtain funding you must register to at least one working group of EuroProofNet, using this link
  3. deadline for funding request applications is May 12
  4. daily allowance for this meeting (including accommodation, meals) is 209 euros
You need to provide the relevant information in the Registration form above.