International Workshop on Programs from Proofs
University of Bath, 15–16 September 2025

This one-off workshop brought together researchers from different backgrounds and traditions who shared a common interest in the computational content of proofs. A particular focus was the application of ideas and techniques from proof theory to systematically extract this content, though the workshop encompassed both theory and application, and covered research across pure mathematics, logic, theoretical computer science, and computer formalised mathematics.

The event was supported by the EPSRC grant Imperative Programs from Proofs and the Department of Computer Science at the University of Bath.

Programme

Talks took place in the Department of Computer Science 1W 2.104. Full details can be found in the book of abstracts.

Monday 15 September

• 0900–0930 Arrival and welcome
• 0930–1020 Ulrich Kohlenbach (TU Darmstadt)
  Logical aspects of proof mining and recent applications to optimization, ergodic theory and difference equations
• 1020–1050 Coffee and discussion
• 1050–1140 Laura Fontanella (Paris Est)
  Realizability models for set theory
• 1140–1230 Pierre-Marie Pedrot (Inria Rennes-Bretagne-Atlantique)
  Π-types and Prejudice
• 1230–1410 Lunch
• 1410–1500 Horatiu Cheval (University of Bucharest)
  Applications of proof mining for program extraction in Lean
• 1500–1550 Morenikeji Neri (TU Darmstadt)
  Oscillations in the laws of large numbers
• 1550–1620 Coffee and discussion
• 1620–1710 Thomas Powell (University of Bath)
  On proof theoretic and quantitative aspects of stochastic processes
• 1830 Workshop dinner: The Architect

Tuesday 16 September

• 0930–1020 Paulo Oliva (Queen Mary University of London)
  Non-deterministic and stochastic selection functions
• 1020–1050 Coffee and discussion
• 1050–1140 Paolo Pistone (ENS Lyon)
  Proof theory for probabilistic termination
• 1140–1230 Guillaume Geoffroy (Université Paris Cité)
  Classical realizability: Characteristic Boolean algebras and nondeterminism
• 1230–1410 Lunch
• 1410–1500 Nicholas Pischke (University of Bath)
  Recent progress in proof mining and probability theory
• 1500–1550 Anupam Das (University of Birmingham)
  On the computational expressivity of type systems with fixed points
• 1550–1620 Coffee and discussion
• 1620–1710 Davide Barbarossa (University of Bath)
  Dialectica realisers and Hoare logic

Organisers

• Davide Barbarossa
• Ben Langton
• Thomas Powell
• Alex Wan