Mathematical logic: proof theory, type theory and constructive mathematics (Q2487181)

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.