Meeting: Proof Systems for Mathematics and Verification

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.

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

Date
June 15 : 9am - 3pm

Venue
EPFL/UNIL Campus in Lausanne

Speakers
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