[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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)
