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 14 : 10am (welcome coffee from 9:15am) - 7pm

Venue
EPFL/UNIL Campus in Lausanne

Speakers
10:00 Assia Mahboubi : Proof transfer for free, beyond type equivalence
11:00 Jeremy Avigad : Mathematical Structures in Dependent Type Theory
14:00 Chelsea L Edmonds : Formal Probabilistic Techniques for Combinatorics in Isabelle/HOL
15:00 Natarajan Shankar : Beautiful Formalizations and Proofs
16:30 Jasmin Blanchette : Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL
17:30 John Harrison (via zoom)

More information