Selected Publications of Helmut Schwichtenberg

Books and Surveys

• Proofs and Computations, with Stanley S. Wainer, 2012 (Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press) Catalogue page at CUP.
• Basic Proof Theory, with Anne Troelstra, 2000 (Cambridge Tracts in Theoretical Computer Science 43). Corrections for the 2nd edition.
• Classifying recursive functions (In Handbook of Computability Theory, Ed. E. Griffor, North-Holland 1999) ps-file

Recent papers

• Towards a formal theory of computability, with S. Huber and B. Karadais (To appear in the Pohlers Festschrift)
• Decorating proofs, with D. Ratiu (To appear in the Mints Festschrift)
• Content in proofs of list reversal (Marktoberdorf '07)
• Dialectica Interpretation of Well-Founded Induction, (Final version in Mathematical Logic Quarterly)
• Proof with Feasible Computational Content (Marktoberdorf '07 working material)
• Realizability interpretation of proofs in constructive analysis, (To appear in ToCS)
• New Developments in Proofs and Computations, (Final version in New Computational Paradigms (B. Cooper, B. Löwe, A. Sorbi, eds.))
• Machine Extraction of the Normalization-by-Evaluation Algorithm from a Normalization Proof, with Dominik Schlenker (Marktoberdorf '05)
• Inverting monotone continuous functions in constructive analysis, (Proc. CiE 2006, Swansea)
• Program extraction in constructive analysis, (Final version in S. Lindström et al., eds, Logicism, Intuitionism, and Formalism -- What has become of them?)
• Recursion on the partial continuous functionals, (Proc. LC 2005, Athens)
• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis, (Final version in J. of Universal Computer Science 11, 2005)
• Program extraction from normalization proofs, with U. Berger, S. Berghofer and P. Letouzey (Final version in Studia Logica 82, 2006)
• Proof search in minimal logic (AISC, 2004)
• Constructive Analysis with Witnesses (Marktoberdorf '03)
• Constructive Solutions of Continuous Equations, with P. Schuster (Russell Volume, 2004)
• An arithmetic for polynomial-time computation (Final version in TCS 357, 2006)
• An arithmetic for non-size-increasing polynomial-time computation, with K. Aehlig, U. Berger and M. Hofmann (Final version in TCS 318, 2004)
• Feasible computation with higher types, with S. Bellantoni (Marktoberdorf '01)
• Linear Ramified Higher Type Recursion and Parallel Computation, with K. Aehlig, J. Johannsen and S. Terwijn (PTCS Volume LNCS 2183, 2001)
• Refined Program Extraction from Classical Proofs, with U. Berger and W. Buchholz (Final version in Annals of Pure and Applied Logic 114, 2002)
• Beweise und Programme. Anmerkungen zu Heytings Formalisierung der intuitionistischen Logik (Ber. Abh. Berlin Brand. Akad. Wiss 8, 2000)
• A syntactical analysis of non-size-increasing polynomial time computation, with K. Aehlig (LICS'2000) ( Journal version, in ACM ToCL)
• Refined Program Extraction from Classical Proofs: Some Case Studies, (Marktoberdorf '99)
• Term rewriting for normalization by evaluation, with U. Berger and M. Eberl (Final version in Information and Computation 183, 2003)
• Higher Type Recursion, Ramification and Polynomial Time, with S. Bellantoni and K-H. Niggl (Final version in Annals of Pure and Applied Logic 104, 2000).
• Normalization by evaluation, with U. Berger and M. Eberl (NADA Volume LNCS 1546, 1998)
• Proof theory at work: Program development in the Minlog system , with H. Benl, U. Berger, M. Seisenberger and W. Zuber (Automated Deduction, W. Bibel and P.H. Schmitt, eds., Vol. II, Kluwer 1998)
• Formal correctness proofs of functional programs: Dijkstra's algorithm, a case study , with H. Benl (Marktoberdorf '97))
• Termination of permutative conversions in intuitionistic Gentzen calculi (Final version in TCS 212, 1999)
• Monotone majorizable functionals (Final version in Studia Logica 62, 1999)
• The Warshall Algorithm and Dickson's Lemma: Two examples of realistic program extraction, with U. Berger and M. Seisenberger (Final version in Journal of Automated Reasoning 26, 2001)
• Programmentwicklung durch Beweistransformation: Das Maximalsegmentproblem (Bayer. Akad., 12/96)
• Finite notations for infinite terms (Final version in Annals of Pure and Applied Logic 94, 1998)
• From higher order terms to circuits, with K. Stroetmann (ICLMPS Florenz '95)
• The greatest common divisor: a case study for program extraction from classical proofs (also in dvi or pdf -format), with U. Berger (Turin '95)
• Proofs, Lambda Terms and Control Operators (Marktoberdorf '95)
• Strict Functionals for Termination Proofs, with J. van de Pol (TLCA '95)
• Program Extraction from Classical Proofs , with U. Berger (LCC '94)
• Ordinal Bounds for Programs, with A. Wainer (Feasible Math '94)
• Density and choice for total continuous functionals (Kreisel '93)
• Program development by proof transformation, with U. Berger (Marktoberdorf '93)
• Minimal from Classical Proofs (CSL '91)
• Minimal Logic for Computable Functions (Marktoberdorf '91)
• Proofs as Programs (Leeds '90)
• An upper bound for reduction sequences in the typed lambda-calculus (Final version in Arch. Math. Logic 30, 1991)
• Normalization (Marktoberdorf '89)
• Primitive Recursion on the Partial Continuous Functionals (Bauer-Kolloquium '89)