Proof Systems for Mathematics and Verification

, EPFL, Lausanne

A joint 2024 meeting of:

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 will be primarily an in-person meeting with talks and breaks for discussions, but we will also provide a Zoom connection for confirmed remote participants.

Program for Friday, June 14

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
12:15 Lunch Break
14:00 Chelsea Edmonds Formal Probabilistic Techniques for Combinatorics in Isabelle/HOL
15:00 Natarajan Shankar
16:00 Coffee
16:30 Jasmin Blanchette Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL
17:30 John Harrison (via zoom)
18:30 Informal Discussion
19:00 Amphitheater Closes

Program for Saturday, June 15

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)
10:00 Carsten Fuhs Proving Equivalence of Imperative Programs via Constrained Rewriting Induction/td>
10:30 Coffee
11:00 Geoff Sutcliffe The TPTP formats for Proofs and Models
11:30 Mathias Fleury Alethe, A flexible proof format with fine-grained steps
12:00 Lunch
14:00 Julian Parsert Guiding Function Synthesis with AI
14:30 Roussanka Loukanova Semantics of Propositional Attitudes in Type-Theory of Algorithms
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:

EPFL Campus Aerial View

International Participants (Partial List)

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 Rennes, France
Fatih Özkaynak Fırat, Turkey
Julian Parsert Innsbruck, Austria
Philipp Rümmer Regensburg, Germany
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

Organizers

Participants from Switzerland

Aurèle Barrière, Prof. Thomas Bourgeat (now at EPFL), Matthieu Bovel, Mario Bucev, Samuel Chassot, Shardul Chiplunkar, Basil Contovounesios, Arnaud Daby-Seesaral, Yawen Guan, Simon Guilloud, Tao Lyu, Prof. George Metcalfe, Dragana Milovancevic, Alexandre Pinazza, Auguste Poiroux, Prof. Maryna Viazovska (wikipedia page), Dominik Winterer, Marcin Wojnarowski

Registration

Please fill this Google form to register. Contact organizers for any questions.

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.