Diese Seite ist aus Gründen der Barrierefreiheit optimiert für aktuelle Browser. Sollten Sie einen älteren Browser verwenden, kann es zu Einschränkungen der Darstellung und Benutzbarkeit der Website kommen!
Books and Surveys
-
Proofs and Computations, with Stanley S. Wainer, 2012 (Perspectives in
Logic, Association for Symbolic Logic and Cambridge University Press).
- 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
Papers
-
Program extraction in exact real arithmetic, with K. Miyamoto.
Submitted (November 2011)
-
Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras,
with U. Berger, K. Miyamoto and M. Seisenberger. To appear: CALCO-Tools 2011
-
Minimal from classical proofs, with C. Senjak. Submitted (March 2011)
-
Towards a formal theory of computability, with S. Huber and B. Karadais
(In: R. Schindler, ed, Pohlers Festschrift, 2010)
-
Decorating proofs, with D. Ratiu
(In: S. Feferman and W. Sieg, eds, Mints Festschrift, 2010)
-
Content in proofs of list reversal
(Marktoberdorf '07)
-
Dialectica Interpretation of Well-Founded Induction,
(Final version in Mathematical Logic Quarterly 54, 2008)
-
Proof with Feasible Computational Content
(Marktoberdorf '07 working material)
-
Realizability interpretation of proofs in constructive analysis,
(Final version in ToCS, 2008)
-
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)
There is also a
List of publications
See also the listing in
Google scholar
Last change: 2011-12-16
Helmut Schwichtenberg,
schwicht[at]math.lmu.de