Program Extraction and Constructive Proofs

A Workshop in Honour of Helmut Schwichtenberg

at MFCS & CSL, Brno, Czech Republic, 21-22 August 2010

held jointly with Classical Logic and Computation

This workshop is to be held on the occasion that Helmut Schwichtenberg will be turning emeritus in September 2010. The workshop will focus on recent developments in Applied Proof Theory and Constructive Mathematics. The two fields have a substantial common interest, namely the exploration of the computational content of mathematical and logical principles. It is the aim of this workshop to bring active researchers from both fields together and exchange ideas. The workshop will also honour Helmut Schwichtenberg's many important contributions to both fields.

Joint key note speakers

Ulrich Kohlenbach

Grigori Mints

Michael Rathjen

Helmut Schwichtenberg

Stan Wainer

Preliminary Programme (PECP, 21 August 2010)

9:00	Opening
9:10	Michael Rathjen,	Finding witnesses for existential theorems in intuitionistic set theories.
10:00	Justus Diller	Functional interpretation of classical and constructive set theory

10:30	Coffee

11:00	Paulo Oliva	Theorems, games, proofs and optimal strategies
11:30	Dieter Spreen	A refined model construction for the polymorphic lambda calculus
12:00	Josef Berger	Binary expansions and quadtrees

12:30	Lunch

14:10	Helmut Schwichtenberg	Proofs and Computations
15:00	Thorsten Altenkirch	Normalisation by Completeness

15:30	Coffee

16:00	Anton Setzer	Extraction of programs from proofs about real numbers in dependent type theory
16:30	Fredrik Forsberg	Formalising inductive-inductive definitions
17:00	Federico Aschieri, Stefano Berardi, Ugo de Liguoro	Monotone Learning, Interactive Realizers and Monads

17:30	Break

17:40	Stan Wainer	A Hierarchy of ``Predicative'' Theories within PRA
18:30	Closing

Preliminary Programme (CLAC, 22 August 2010)

9:00	Opening
9:10	Grigori Mints	Epsilon substitution in predicate logic
10:00	Frederico Aschieri	Interactive learning based realizability and 1-backtracking games

10:30	Coffee

11:00	Luis Pinto and Tarmo Uustalu	Relating sequent calculi for bi-intuitistic propositional logic
11:30	Clement Houtman	Superdeduction in lambda bar mu mu tilde
12:00	Reinhard Kahle and Isabel Oitavem	An applicative theory for PH

12:30	Lunch
14:10	Ulrich Kohlenbach	Analyzing proofs based on weak sequential compactness
15:00	Trifon Trifonov	Dialectica interpretation with marked counterexamples

15:30	Coffee

16:00	Gilda Ferreira and Paulo Oliva	On various negative translations
16:30	Jeffrey Vaughan	A logical interpretation of Java-style exceptions
16:50	Stefan Hetzl, Alexander Leitsch and Daniel Weller	CERES in higher-order logic
17:10	Closing

PECP Keynote speakers, invited speakers and invited participants

Thorsten Altenkirch (Nottingham), Stefano Berardi (Torino), Josef Berger (Munich), Justus Diller (Munster), Gilda Ferreira (London), Fredrik Forsberg (Swansea), Reinhard Kahle (Lisboa), Ulrich Kohlenbach (Darmstadt), Grigori Mints (Standford), Paulo Oliva (London), Isabel Oitavem (Lisboa), Michael Rathjen (Leeds), Helmut Schwichtenberg (Munich), Anton Setzer (Swansea), Dieter Spreen (Siegen). Trifon Trifonov (Sofia), Stan Wainer (Leeds), Wolfgang Zuber. (Further participants to be added.)

Venue

The main conference and its satellite workshops will be held in the main building of the Faculty of Informatics of Masaryk University. (See travel pages of the conference for maps how to get here).