[TYPES/announce] Programs from Proofs Meets Formal Mathematics - call for participation

[Thomas Powell]

WORKSHOP ON PROGRAMS FROM PROOFS MEETS FORMAL MATHEMATICS 
Part of ESSLLI 2025, Ruhr University Bochum, July 28 - August 1, 2025
Website: https://urldefense.com/v3/__https://t-powell.github.io/ppfm/ppfm.html__;!!IBzWLUs!QxW13DVviRh7JeAjHPFKqQWiKv2dmAmRRAxyucBUU-sobWxO8tZHlE1Lo4GgUudzZL9EKmk2GDKk0DYZXNqmkbV_5EPDXPs4$ 

ABOUT THE WORKSHOP

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 from proof theory, such as 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.

ABOUT ESSLLI

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.

The European Summer School in Logic, Language and Information (ESSLLI) is a yearly recurring event, which has been organized since 1989. An ESSLLI Summer School provides an interdisciplinary setting in which courses and workshops are offered in logic, linguistics and computer science. The whole event lasts two weeks and is organized under the auspices of the Association for Logic, Language and Information (FoLLI).

See https://urldefense.com/v3/__https://2025.esslli.eu/__;!!IBzWLUs!QxW13DVviRh7JeAjHPFKqQWiKv2dmAmRRAxyucBUU-sobWxO8tZHlE1Lo4GgUudzZL9EKmk2GDKk0DYZXNqmkbV_5N-nYX9I$ 

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:

- Proof theory and its applications, particularly the extraction of programs from proofs.
- Logical systems for reasoning about mathematics or the sciences.
- Proof assistants (e.g. Adga, Coq, Isabelle, Lean).
- Applications of AI and machine learning to formal mathematics.

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 https://urldefense.com/v3/__https://2025.esslli.eu/registration/travel-grants.html__;!!IBzWLUs!QxW13DVviRh7JeAjHPFKqQWiKv2dmAmRRAxyucBUU-sobWxO8tZHlE1Lo4GgUudzZL9EKmk2GDKk0DYZXNqmkbV_5Mf3idye$ 

IMPORTANT DATES

-   6 January 2024: Abstract submission opens
-   15 April 2025: Deadline for abstract submission
-   1 May 2025: Notification of acceptance
-   31 May 2025: ESSLLI early registration deadline
-   July 28 - August 1 2025: Workshop

With best wishes,

Nicholas Pischke and Thomas Powell (organizers)