Contributions:
– Ulrich Kohlenbach, Proof mining: applications of proof theory to analysis p.783
– Paulo Oliva, A parametrized functional interpretation p.785
– Ulrich Berger, Strong normalization for applied lambda calculi p.785
– Lev Beklemishev, On \(\Sigma_2\)-theorems of fragments of PA p.785
– Giovanni Sambin, Towards a minimalistic foundation of constructive mathematics p.786
– Gilles Dowek, Cut elimination in set theory p.786
– Klaus Aehlig (joint with Jolie G. de Miranda and C.-H. Luke Ong), Level-two recursion schemes and finite automata p.786
– Stephen A. Cook, Making sense of bounded arithmetic: a complexity theorist’s point of view p.787
– Jan Krajíček, Forcing with random variables p.788
– Chris Pollett (joint with Norman Danner), Equivalents of the weak multifunction pigeonhole principle p.789
– Peter Aczel, Topology in constructive set theory (background and motivations) p.790
– Michael Rathjen, The disjunction property for CZF p.793
– Thomas Streicher, Realizability models for CZF + \(\lnot\)Pow p.793
– Sara Negri, Cut elimination in provability logic p.793
– Fernando Ferreira, Majorisability interpretations in finite-type arithmetic p.794
– Laurentiu Leustean (joint with Ulrich Kohlenbach), Approximate fixed point property in product spaces p.795
– Philipp Gerhardy, A case study in proof mining: an effective version of Kirk’s fixed-point theorem for asymptotic contractions p.797
– Thierry Coquand, Infinite objects in constructive mathematics: applications of proof theory to algebra p.797
– Joan Rand Moschovakis, The effect of Markov’s Principle on the intuitionistic continuum p.797
– Peter Schuster (joint with Josef Berger), Classifying Dini’s Theorem p.799
– Gigori Mints (joint with Henry Towsner), An epsilon substitution method with finite sets p.801
– Rosalie Iemhoff, Skolemization in intuitionistic logic p.801
– Albert Visser, Categories of interpretation p.802
– Isabel Oitavem, Implicit characterizations p.802
– Arnold Beckmann, Bounded arithmetic, definable functions and dynamic ordinals p.803
– Dirk Pattinson, Domain-theoretic construction of inverse functions p.804
– Thomas Strahm, On the proof theory of type two functionals p.804
– Tarmo Uustalu (joint with Thorsten Altenkirch, Venanzio Capretta), Partiality via coinductive types p.805
– Ralph Matthes, Monadic stabilization for operationalized second-order classical logic with disjunction and permutative conversions p.805
– Andreas Weiermann, Phase transitions in logic and Ramsey theory p.807
– Anton Setzer, Towards a more algebraic treatment of ordinal notation systems p.808
– Sergei Tupailo, Monotone inductive definitions and the consistency of New Foundations p.808.