## 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)
See also the listing in Google scholar Last change: 2011-12-16 Helmut Schwichtenberg, schwicht[at]math.lmu.de |