Bibliography

1

P. Aczel, H. Simmons, and S.S. Wainer, editors.
Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990. Cambridge University Press, 1992.

2

Klaus Aehlig, Ulrich Berger, Martin Hofmann, and Helmut Schwichtenberg.
An arithmetic for non-size-increasing polynomial time computation.
Theoretical Computer Science, 318(1-2):3-27, 2004.

3

Klaus Aehlig, Jan Johannsen, Helmut Schwichtenberg, and Sebastiaan Terwijn.
Linear ramified higher type recursion and parallel computation.
In R. Kahle, P. Schröder-Heister, and R. Stärk, editors, Proof Theory in Computer Science, volume 2183 of LNCS, pages 2-21. Springer Verlag, Berlin, Heidelberg, New York, 2001.

4

Klaus Aehlig and Helmut Schwichtenberg.
A syntactical analysis of non-size-increasing polynomial time computation.
In Proceedings 15'th Symposium on Logic in Computer Science (LICS 2000), pages 84-91, 2000.

5

Klaus Aehlig and Helmut Schwichtenberg.
A syntactical analysis of non-size-increasing polynomial time computation.
ACM Transactions of Computational Logic, 3(3):383-401, 2002.

6

Stephen Bellantoni, Karl-Heinz Niggl, and Helmut Schwichtenberg.
Higher type recursion, ramification and polynomial time.
Annals of Pure and Applied Logic, 104:17-30, 2000.

7

Holger Benl, Ulrich Berger, Helmut Schwichtenberg, Monika Seisenberger, and Wolfgang Zuber.
Proof theory at work: Program development in the Minlog system.
In W. Bibel and P.H. Schmitt, editors, Automated Deduction - A Basis for Applications, volume II: Systems and Implementation Techniques of Applied Logic Series, pages 41-71. Kluwer Academic Publishers, Dordrecht, 1998.

8

Holger Benl and Helmut Schwichtenberg.
Formal correctness proofs of functional programs: Dijkstra's algorithm, a case study.
In U. Berger and H. Schwichtenberg, editors, Computational Logic, volume 165 of Series F: Computer and Systems Sciences, pages 113-126. Proceedings of the NATO Advanced Study Institute on Computational Logic, held in Marktoberdorf, Germany, July 29 - August 10, 1997, Springer Verlag, Berlin, Heidelberg, New York, 1999.

9

Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg.
Program extraction from normalization proofs.
Studia Logica, 82:27-51, 2006.

10

Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg.
Refined program extraction from classical proofs.
Annals of Pure and Applied Logic, 114:3-25, 2002.

11

Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg.
Normalization by evaluation.
In B. Möller and J.V. Tucker, editors, Prospects for Hardware Foundations, volume 1546 of LNCS, pages 117-137. Springer Verlag, Berlin, Heidelberg, New York, 1998.

12

Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg.
Term rewriting for normalization by evaluation.
Information and Computation, 183:19-42, 2003.

13

Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Monika Seisenberger.
Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras.
In Corina Cirstea Andrea Corradini, Bartek Kli, editor, Algebra and Coalgebra in Computer Science, CALCO'11, volume 6859 of LNCS, pages 393-399. Springer, 2011.

14

Ulrich Berger and Helmut Schwichtenberg.
An inverse of the evaluation functional for typed $\lambda$-calculus.
In R. Vemuri, editor, Proceedings 6'th Symposium on Logic in Computer Science (LICS '91), pages 203-211. IEEE Computer Society Press, Los Alamitos, 1991.

15

Ulrich Berger and Helmut Schwichtenberg.
Program development by proof transformation.
In H. Schwichtenberg, editor, Proof and Computation, volume 139 of Series F: Computer and Systems Sciences, pages 1-45. NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20 - August 1, 1993, Springer Verlag, Berlin, Heidelberg, New York, 1995.

16

Ulrich Berger and Helmut Schwichtenberg.
Program extraction from classical proofs.
In D. Leivant, editor, Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, IN, USA, October 1994, volume 960 of LNCS, pages 77-97. Springer Verlag, Berlin, Heidelberg, New York, 1995.

17

Ulrich Berger and Helmut Schwichtenberg.
The greatest common divisor: a case study for program extraction from classical proofs.
In S. Berardi and M. Coppo, editors, Types for Proofs and Programs. International Workshop TYPES '95, Torino, Italy, June 1995. Selected Papers, volume 1158 of LNCS, pages 36-46. Springer Verlag, Berlin, Heidelberg, New York, 1996.

18

Ulrich Berger, Helmut Schwichtenberg, and Monika Seisenberger.
The Warshall algorithm and Dickson's lemma: two examples of realistic program extraction.
Journal of Automated Reasoning, 26:205-221, 2001.

19

Peter G. Clote and Helmut Schwichtenberg, editors.
Computer Science Logic. 14th International Workshop, CSL 2000, volume 1862 of LNCS. Springer Verlag, Berlin, Heidelberg, New York, 2000.

20

Simon Huber, Basil A. Karádais, and Helmut Schwichtenberg.
Towards a formal theory of computability.
In R. Schindler, editor, Ways of Proof Theory: Festschrift for W. Pohlers, pages 251-276. Ontos Verlag, 2010.

21

Diana Ratiu and Helmut Schwichtenberg.
Decorating proofs.
In S. Feferman and W. Sieg, editors, Proofs, Categories and Computations. Essays in honor of Grigori Mints, pages 171-188. College Publications, 2010.

22

Dieter Rödding and Helmut Schwichtenberg.
Bemerkungen zum Spektralproblem.
Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 18:1-12, 1972.

23

Peter Schuster and Helmut Schwichtenberg.
Constructive solutions of continuous equations.
In G. Link, editor, One Hundred Years of Russell's Paradox. International Conference in Logic and Philosophy. Munich, Germany, June 2-5, 2001, pages 227-245. de Gruyter, 2004.

24

Kurt Schütte and Helmut Schwichtenberg.
Mathematische Logik.
In W. Scharlau G. Fischer, F. Hirzebruch and W. Törnig, editors, Ein Jahrhundert Mathematik 1890-1990. Festschrift zum Jubiläum der DMV, volume 6 of Dokumente zur Geschichte der Mathematik, pages 717-740. Vieweg, Brauschweig/Wiesbaden, 1990.

25

H. Schwichtenberg and K. Spies, editors.
Proof Technology and Computation. Proc. NATO Advanced Study Institute, Marktoberdorf, 2003, volume 200 of Series III: Computer and Systems Sciences. IOS Press, 2006.

26

Helmut Schwichtenberg.
Eine Klassifikation der mehrfach-rekursiven Funktionen.
PhD thesis, Mathematisches Institut der Universität Münster, 1968.

27

Helmut Schwichtenberg.
Rekursionszahlen und die Grzegorczyk-Hierarchie.
Archiv für Mathematische Logik und Grundlagenforschung, 12:85-97, 1969.

28

Helmut Schwichtenberg.
Eine Klassifikation der $\epsilon_0$-rekursiven Funktionen.
Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 17:61-74, 1971.

29

Helmut Schwichtenberg.
Beweistheoretische Charakterisierung einer Erweiterung der Grzegorczyk-Hierarchie.
Archiv für Mathematische Logik und Grundlagenforschung, 15:129-145, 1972.

30

Helmut Schwichtenberg.
Einige Anwendungen von unendlichen Termen und Wertfunktionalen.
Habilitationsschrift, Mathematisches Institut der Universität Münster, 1973.

31

Helmut Schwichtenberg.
Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion.
In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, pages 279-303. North-Holland, Amsterdam, 1975.

32

Helmut Schwichtenberg.
Definierbare Funktionen im $\lambda$-Kalkül mit Typen.
Archiv für Mathematische Logik und Grundlagenforschung, 17:113-114, 1976.

33

Helmut Schwichtenberg.
Proof theory: some applications of cut-elimination.
In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter Proof Theory and Constructive Mathematics, pages 867-895. North-Holland, Amsterdam, 1977.

34

Helmut Schwichtenberg.
Logic and the axiom of choice.
In M. Boffa et al., editors, Logic Colloquium '78, pages 351-356. North-Holland, Amsterdam, 1978.

35

Helmut Schwichtenberg.
On bar recursion of types 0 and 1.
The Journal of Symbolic Logic, 44:325-329, 1979.

36

Helmut Schwichtenberg.
Complexity of normalization in the pure typed $\lambda$-calculus.
In A.S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hald in Noordwijkerhout, 8-13 June, 1981, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 453-458. North-Holland, Amsterdam, 1982.

37

Helmut Schwichtenberg.
Ein einfaches Verfahren zur Normalisierung unendlicher Herleitungen.
In E. Börger, editor, Computation Theory and Logic, volume 270 of LNCS, pages 334-348. Springer Verlag, Berlin, Heidelberg, New York, 1986.

38

Helmut Schwichtenberg.
Eine Normalform für endliche Approximationen von partiellen stetigen Funktionalen.
In J. Diller, editor, Logik und Grundlagenforschung, Festkolloquium zum 100. Geburtstag von Heinrich Scholz, pages 89-95, 1986.

39

Helmut Schwichtenberg.
A normal form for natural deductions in a type theory with realizing terms.
In V.M Abrusci and E. Casari, editors, Atti del Congresso Logica e Filosofia della Scienza, oggi, San Gimignano, 7-11 dicembre 1983, Vol.1-Logica, pages 95-138, Bologna, 1986. CLUEB.

40

Helmut Schwichtenberg.
Mathematische Logik.
In Mathematik, volume 10, pages 39-42. TU Berlin, Berlin, 1987.

41

Helmut Schwichtenberg.
Normalization.
In F.L. Bauer, editor, Logic, Algebra and Computation. Proceedings of the International Summer School Marktoberdorf, Germany, July 25 - August 6, 1989, Series F: Computer and Systems Sciences, Vol. 79, pages 201-237. NATO Advanced Study Institute, Springer Verlag, Berlin, Heidelberg, New York, 1991.

42

Helmut Schwichtenberg.
Primitive recursion on the partial continuous functionals.
In M. Broy, editor, Informatik und Mathematik, pages 251-269. Springer Verlag, Berlin, Heidelberg, New York, 1991.

43

Helmut Schwichtenberg.
An upper bound for reduction sequences in the typed $\lambda$-calculus.
Archive for Mathematical Logic, 30:405-408, 1991.
Dedicated to Kurt Schütte on the occasion of his 80th birthday.

44

Helmut Schwichtenberg.
Minimal from classical proofs.
In E. Börger, G. Jäger, H. Kleine-Büning, and M.M. Richter, editors, Computer Science Logic, volume 626 of LNCS, pages 326-328. Springer Verlag, Berlin, Heidelberg, New York, 1992.

45

Helmut Schwichtenberg.
Proofs as programs.
In Aczel et al. [1], pages 81-113.

46

Helmut Schwichtenberg.
Minimal logic for computable functions.
In F.L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, volume 94 of Series F: Computer and Systems Sciences, pages 289-320. NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 23-August 4, 1991, Springer Verlag, Berlin, Heidelberg, New York, 1993.

47

Helmut Schwichtenberg.
Density and choice for total continuous functionals.
In P. Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 335-362. A.K. Peters, Wellesley, Massachusetts, 1996.

48

Helmut Schwichtenberg.
Programmentwicklung durch Beweistransformation: Das Maximalsegmentproblem.
Sitzungsber. d. Bayer. Akad. d. Wiss., Math.-Nat. Kl., pages 8*-12*, 1997.

49

Helmut Schwichtenberg.
Proofs, lambda terms and control operators.
In H. Schwichtenberg, editor, Logic of Computation, volume 157 of Series F: Computer and Systems Sciences, pages 309-347. Proceedings of the NATO Advanced Study Institute on Logic of Computation, held in Marktoberdorf, Germany, July 25 - August 6, 1995, Springer Verlag, Berlin, Heidelberg, New York, 1997.

50

Helmut Schwichtenberg.
Finite notations for infinite terms.
Annals of Pure and Applied Logic, 94:201-222, 1998.

51

Helmut Schwichtenberg.
Classifying recursive functions.
In E. Griffor, editor, Handbook of Computability Theory, pages 533-586. North-Holland, Amsterdam, 1999.

52

Helmut Schwichtenberg.
Monotone majorizable functionals.
Studia Logica, 62:283-289, 1999.

53

Helmut Schwichtenberg.
Termination of permutative conversions in intuitionistic Gentzen calculi.
Theoretical Computer Science, 212:247-260, 1999.

54

Helmut Schwichtenberg.
Beweise und Programme. Anmerkungen zu Heytings Formalisierung der intuitionistischen Logik.
Berichte und Abhandlungen der Berlin-Brandenburgischen Akademie der Wissenschaften, 8:71-94, 2000.

55

Helmut Schwichtenberg.
Refined program extraction from classical proofs: Some case studies.
In F.L. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 147-166, Amsterdam, 2000. IOS Press.

56

Helmut Schwichtenberg.
Proof search in minimal logic.
In B. Buchberger and J.A. Campbell, editors, Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 2004, Proceedings, volume 3249 of LNAI, pages 15-25. Springer Verlag, Berlin, Heidelberg, New York, 2004.

57

Helmut Schwichtenberg.
A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis.
Journal of Universal Computer Science, 11(12):2086-2095, 2005.
http://www.jucs.org/jucs_11_12/a_direct_proof_of.

58

Helmut Schwichtenberg.
An arithmetic for polynomial-time computation.
Theoretical Computer Science, 357:202-214, 2006.

59

Helmut Schwichtenberg.
Constructive analysis with witnesses.
In Schwichtenberg and Spies [25], pages 323-353.

60

Helmut Schwichtenberg.
Inverting monotone continuous functions in constructive analysis.
In A. Beckmann, U. Berger, B. Löwe, and J.V. Tucker, editors, Logical Approaches to Computational Barriers. (Proc. CiE 2006, Swansea), volume 3988 of LNCS, pages 490-504. Springer Verlag, Berlin, Heidelberg, New York, 2006.

61

Helmut Schwichtenberg.
Minlog.
In F. Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of LNAI, pages 151-157. Springer Verlag, Berlin, Heidelberg, New York, 2006.

62

Helmut Schwichtenberg.
Recursion on the partial continuous functionals.
In C. Dimitracopoulos, L. Newelski, D. Normann, and J. Steel, editors, Logic Colloquium '05, volume 28 of Lecture Notes in Logic, pages 173-201. Association for Symbolic Logic, 2006.

63

Helmut Schwichtenberg.
Content in proofs of list reversal.
In O. Grumberg, T. Nipkow, and C. Pfaller, editors, Formal Logical Methods for System Security and Correctness. Proc. NATO Advanced Study Institute, Marktoberdorf, 2007, pages 267-285. IOS Press, 2008.

64

Helmut Schwichtenberg.
Dialectica interpretation of well-founded induction.
Math. Logic. Quarterly, 54(3):229-239, 2008.

65

Helmut Schwichtenberg.
New developments in proofs and computations.
In A. Sorbi B. Cooper, B. Löwe, editor, New Computational Paradigms, pages 313-340. Springer Verlag, Berlin, Heidelberg, New York, 2008.

66

Helmut Schwichtenberg.
Program extraction in constructive analysis.
In S. Lindström, E.Palmgren, K. Segerberg, and V. Stoltenberg-Hansen, editors, Logicism, Intuitionism, and Formalism - What has become of them?, pages 251-271. Springer Verlag, Berlin, Heidelberg, New York, 2008.

67

Helmut Schwichtenberg.
Realizability interpretation of proofs in constructive analysis.
Theory of Computing Systems, 43(3):583-602, 2008.

68

Helmut Schwichtenberg and Stephen Bellantoni.
Feasible computation with higher types.
In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and System-Reliability, Proceedings NATO Advanced Study Institute, Marktoberdorf, 2001, pages 399-415. Kluwer Academic Publisher, 2002.

69

Helmut Schwichtenberg and Christoph Senjak.
Minimal from classical proofs.
To appear in APAL, 2012.

70

Helmut Schwichtenberg and Karl Stroetmann.
From higher order terms to circuits.
In M.L. Dalla Chiara, K. Doets, D. Mundici, and J. van Benthem, editors, Logic and Scientific Methods. Proceedings (Vol. 1) of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995, volume 259 of Synthese Library, pages 209-220, Dordrecht, Boston, London, 1997. Kluwer Academic Publishers.

71

Helmut Schwichtenberg and Stanley S. Wainer.
Infinite terms and recursion in higher types.
In J. Diller and G.H. Müller, editors, Proof Theory Symposion Kiel 1974, volume 500 of Lecture Notes in Mathematics, pages 341-364. Springer Verlag, Berlin, Heidelberg, New York, 1975.

72

Helmut Schwichtenberg and Stanley S. Wainer.
Ordinal bounds for programs.
In P. Clote and J. Remmel, editors, Feasible Mathematics II, pages 387-406. Birkhäuser, Boston, 1995.

73

Helmut Schwichtenberg and Stanley S. Wainer.
Proofs and Computations.
Perspectives in Logic. Association for Symbolic Logic and Cambridge University Press, 2012.

74

Anne S. Troelstra and Helmut Schwichtenberg.
Basic Proof Theory.
Cambridge University Press, second edition, 2000.

75

Jaco van de Pol and Helmut Schwichtenberg.
Strict functionals for termination proofs.
In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of LNCS, pages 350-364. Springer Verlag, Berlin, Heidelberg, New York, 1995.