Workshop on programs from proofs meets formal mathematics
Part of ESSLLI 2025, Ruhr University Bochum
The workshop will run during Week 1 of ESSLLI (July 28 – August 1), from 11:00 – 12:30 in Room GB 03/49.
The aim of this workshop is to provide a discussion forum and an opportunity to meet others who have a broad interest in logic and proof assistants.
A focus will be on how methods for program extraction, particularly 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.
However, the workshop is open to all participants of ESSLLI. In particular, if you would like to either
you are encouraged to take part.
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.