Proof Systems for Mathematics and Verification

June 14-15, 2024, EPFL, Lausanne (see some views from above)

A joint 2024 meeting of:

Updates:

A page with a few picture highlights from the event is available.
Video recordings and slides are available for many of the talk; see the links in the program below.

Purpose

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

Location

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:

the event place, amphitheater BCH 2201, on the map of the EPFL campus (a large building across the street from the Bernoulli center)
walking directions from the M1 metro "UNIL Sorge" stop to the building (east level 2 entrance)
walking directions from the SwissTech hotel passing by the Rolex Learning Center, a signature building on the EPFL campus

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

Organizers

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:

SwissTech hotel (use the code "Proofs and Computation", verified rate)
Starling Hotel (usually more expensive and quiet)

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:

"Lausanne, gare" (train station) to "Lausanne-Flon, pl. de l'Europe" (location of ibis Styles hotel): 1 minute via M2 metro
"Lausanne-Flon, pl. de l'Europe" to "Ecublens VD, EPFL" (EPFL campus stop and the location of the SwissTech hotel) 13 minutes via M1 metro

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:

the reimbursement rules of EuroProofNet apply
to obtain funding you must register to at least one working group of EuroProofNet, using this link
deadline for funding request applications is May 12
daily allowance for this meeting (including accommodation, meals) is 209 euros

You need to provide the relevant information in the Registration form above.