Meeting: Proof Systems for Mathematics and Verification


Event details

Date 15.06.2024
Hour 09:0015:00
Location Online
Category Conferences - Seminars
Event Language English

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.

Promote and compare proof systems in formal verification, logic, and mathematics.

June 15 : 9am - 3pm

EPFL/UNIL Campus in Lausanne

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>
11:00 Geoff Sutcliffe : The TPTP formats for Proofs and Models
11:30 Mathias Fleury : Alethe, A flexible proof format with fine-grained steps
14:00 Julian Parsert : Guiding Function Synthesis with AI
14:30 Roussanka Loukanova : Semantics of Propositional Attitudes in Type-Theory of Algorithms

More information

Practical information

  • General public
  • Free


  • Jacques Duparc, UNIL/EPFL
    Viktor Kuncak, EPFL
    Clément Pit-Claudel, EPFL


  • Viktor Kuncak, EPFL

Event broadcasted in