Workshop on programs from proofs meets formal mathematics
Part of ESSLLI 2025, Ruhr University Bochum, July 28 – August 1, 2025

The aim of this workshop is to bring together experts in proof theory with specialists in formal mathematics and automated theorem proving, in order to facilitate an interdisciplinary exchange of ideas on the mutual benefit that these areas can have on one another.

On the one hand, the workshop will focus on how methods for program extraction, particularly advanced techniques aimed at extracting computational content from large scale nonconstructive proofs in mainstream mathematics, can be implemented and partially automated within theorem provers. In the other direction, we will explore whether the rich variety of logical systems developed by proof theorists could benefit the world of formal mathematics by both simplifying and streamlining the formalisation process.

The event is part of the 36th European Summer School in Logic, Language and Information, where we are the only workshop representing the Logic and Computation stream.

Participation

We welcome 30 minute contributed talks on any topic broadly within the scope of the workshop. We are particularly interested in work that explores the following themes and their intersection:

Presentations from research students and early career researchers are particularly encouraged. To propose a talk, please submit your title and abstract by email to one of the organisers. We put no restrictions on the originality or publication status of submissions. There will be no formal proceedings.

Details about registration, along with local information, are available from the main ESSLLI webpages.

As a part of ESSLLI, our workshop benefits from the funding opportunities offered for PhD students for the whole event. See travel grants for further information.

Important dates

Invited speakers

To be announced...

Organisers