BIBLIOGRAPHY
Published online by Cambridge University Press: 05 January 2012
Summary
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
- Type
- Chapter
- Information
- Proofs and Computations , pp. 431 - 456Publisher: Cambridge University PressPrint publication year: 2011
References
and [2000] A predicative strong normalization proof for a λ-calculus with interleaving inductive types, Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 1956, Springer Verlag, Berlin, pp. 21–40.Google Scholar
[1991] Domain theory in logical form, Annals of Pure and Applied Logic, vol. 51, pp. 1–77.Google Scholar
and [1994] Domain theory, Handbook of Logic in Computer Science (, , and , editors), vol. 3, Clarendon Press, pp. 1–168.
[1940] Zur Widerspruchsfreiheit der Zahlentheorie, Mathematische Annalen, vol. 117, pp. 162–194.Google Scholar
, , and [1992] Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, Cambridge University Press.
and [2005] An elementary fragment of second-order lambda calculus, ACM Transactions on Computational Logic, vol. 6, pp. 468–480.Google Scholar
[1991] A slow growing analogue to Buchholz' proof, Annals of Pure and Applied Logic, vol. 54, pp. 101–120.Google Scholar
[2000] Ordinal diagrams for recursively Mahlo universes, Archive for Mathematical Logic, vol. 39, no. 5, pp. 353–391.Google Scholar
[2000] Interpreting classical theories in constructive ones, The Journal of Symbolic Logic, vol. 65, no. 4, pp. 1785–1812.Google Scholar
and [1997] A model theoretic approach to ordinal analysis, The Bulletin of Symbolic Logic, vol. 3, pp. 17–52.Google Scholar
and [1993] Extracting constructive content from classical logic via control-like reductions, Typed Lambda Calculi and Applications ( and , editors), Lecture Notes in Computer Science, vol. 664, Springer|Verlag, Berlin, pp. 45–59.Google Scholar
, , and [1983] A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol. 48, no. 4, pp. 931–940.Google Scholar
, , and [2003] Ordinal notations and well-orderings in bounded arithmetic, Annals of Pure and Applied Logic, vol. 120, pp. 197–223.Google Scholar
and [1996] A term rewriting characterization of the polytime functions and related complexity classes, Archive for Mathematical Logic, vol. 36, pp. 11–30.Google Scholar
[2003] Proof-theoretic analysis of iterated reflection, Archive for Mathematical Logic, vol. 42, no. 6, pp. 515–552.Google Scholar
and [1992] A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol. 2, pp. 97–110.Google Scholar
and [2002] A new “feasible” arithmetic, The Journal of Symbolic Logic, vol. 67, no. 1, pp. 104–116.Google Scholar
, , and [2000] Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol. 104, pp. 17–30.Google Scholar
[1998] Konstruktive Interpretation induktiver Definitionen, Master's thesis, Mathematisches Institut der Universität München.
[1993a] Program extraction from normalization proofs, Typed Lambda Calculi and Applications ( and , editors), Lecture Notes in Computer Science, vol. 664, Springer Verlag, Berlin, pp. 91–106.Google Scholar
[1993b] Total sets and objects in domain theory, Annals of Pure and Applied Logic, vol. 60, pp. 91–117.Google Scholar
[2005a] Continuous semantics for strong normalization, Proceedings CiE 2005, Lecture Notes in Computer Science, vol. 3526, pp. 23–34.Google Scholar
[2005b] Uniform Heyting arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 125–148.Google Scholar
[2009] From coinductive proofs to exact real arithmetic, Computer Science Logic ( and , editors), Lecture Notes in Computer Science, Springer Verlag, Berlin, pp. 132–146.Google Scholar
, , , and [2006] Program extraction from normalization proofs, Studia Logica, vol. 82, pp. 27–51.Google Scholar
, , and [2002] Refined program extraction from classical proofs, Annals of Pure and Applied Logic, vol. 114, pp. 3–25.Google Scholar
, , and [2003] Term rewriting for normalization by evaluation, Information and Computation, vol. 183, pp. 19–42.Google Scholar
and [1991] An inverse of the evaluation functional for typed λ-calculus, Proceedings 6'th Symposium on Logic in Computer Science (LICS'91) (, editor), IEEE Computer Society Press, Los Alamitos, pp. 203–211.Google Scholar
, , and [2001] The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction, Journal of Automated Reasoning, vol. 26, pp. 205–221.Google Scholar
[1956] Semantic construction of intuitionistic logic, Medelingen de KNAW N.S., vol. 19, no. 11.Google Scholar
and [1993] Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics, Journal of the London Mathematical Society, vol. 47, pp. 193–211.Google Scholar
, , and [1999] The Calculus of Algebraic Constructions, RTA '99, Lecture Notes in Computer Science, vol. 1631.Google Scholar
, , and [1997] The Classical Decision Problem, Perspectives in Mathematical Logic, Springer Verlag, Berlin.Google Scholar
and [1971] Subrecursive programming languages II: on program size, Journal of Computer and System Sciences, vol. 5, pp. 315–334.Google Scholar
[2009] Brief introduction to unprovability, Logic colloquium 2006, Lecture Notes in Logic, Association for Symbolic Logic and Cambridge University Press, pp. 38–64.
[1980] Three contributions to the conference on recent advances in proof theory, Handwritten notes.
[1987] An independence result for –CA+BI, Annals of Pure and Applied Logic, vol. 33, no. 2, pp. 131–155.Google Scholar
, , and [1994] A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 40, pp. 273–286.Google Scholar
, , , and [1981] Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Mathematics, vol. 897, Springer|Verlag, Berlin, Berlin.Google Scholar
and [1978] Provable wellorderings of formal theories for transfinitely iterated inductive definitions, The Journal of Symbolic Logic, vol. 43, pp. 118–125.Google Scholar
and [1987] Provably computable functions and the fast growing hierarchy, Logic and Combinatorics (, editor), Contemporary Mathematics, vol. 65, American Mathematical Society, pp. 179–198.Google Scholar
[1986] Bounded Arithmetic, Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli.Google Scholar
[1994] The witness function method and provably recursive functions of Peano arithmetic, Proceedings of the 9th International Congress of Logic, Methodology and Philosophy of Science (, , and , editors), North-Holland, Amsterdam, pp. 29–68.Google Scholar
[1998a] First order proof theory of arithmetic, Handbook of Proof Theory (, editor), North-Holland, Amsterdam, pp. 79–147.Google Scholar
[1998b] Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam.Google Scholar
, , and [2000] Proof theoretic complexity of low subrecursive classes, Foundations of Secure Computation ( and , editors), NATO Science Series F, vol. 175, IOS Press, pp. 249–285.Google Scholar
[2002] Polytime, combinatory logic and positive safe induction, Archive for Mathematical Logic, vol. 41, no. 2, pp. 169–189.Google Scholar
[2001] Elementary patterns of resemblance, Annals of Pure and Applied Logic, vol. 108, pp. 19–77.Google Scholar
[1976] Constructive operators of finite types, Journal of Mathematical Science, vol. 6, pp. 465–470, translated from Zapiski Nauch. Sem. Leningrad, vol. 32, pp. 140–147 (1972).Google Scholar
[2009] Program Development by Proof Transformation, PhD thesis, Fakultät f ür Mathematik, Informatik und Statistik der LMU,München.
[1936] A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1, pp. 40–41, Correction, ibid., pp. 101–102.Google Scholar
[1983] A short proof of two recently discovered independence proofs using recursion theoretic methods, Proceedings of the American Mathematical Society, vol. 87, pp. 704–706.Google Scholar
[1963] A hierarchy of primitive recursive functions, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 9, pp. 331–345.Google Scholar
and [1995] First order bounded arithmetic and small boolean circuit complexity classes, Feasible Mathematics II ( and , editors), Birkhäuser, Boston, pp. 154–218.Google Scholar
[1965] The intrinsic computational difficulty of functions, Logic, Methodology and Philosophy of Science II (, editor), North-Holland, Amsterdam, pp. 24–30.Google Scholar
[1972] Subrecursive programming languages I: efficiency and program structure, Journal of the ACM, vol. 19, pp. 526–568.Google Scholar
and [1991] Finding computational content in classical proofs, Logical Frameworks ( and , editors), Cambridge University Press, pp. 341–362.Google Scholar
and [1990] Characterizations of the basic feasible functionals of finite type, Feasible Mathematics ( and , editors), Birkhäuser, pp. 71–96.Google Scholar
[2009] The Coq Proof Assistant Reference Manual – Version 8.2, Inria.
and [1999] A new method for establishing conservativity of classical systems over their intuitionstic version, Mathematical Structures in Computer Science, vol. 9, pp. 323–333.Google Scholar
and [1999] Gröbner bases in type theory, Types for Proofs and Programs (, , and , editors), Lecture Notes in Computer Science, vol. 1657, Springer Verlag, Berlin.Google Scholar
, , , and [2003] Inductively generated formal topologies, Annals of Pure and Applied Logic, vol. 124, pp. 71–106.Google Scholar
and [2006] A proof of strong normalisation using domain theory, Proceedings LICS 2006, pp. 307–316.Google Scholar
[1930] Grundlagen der kombinatorischen Logik, American Journal of Mathematics, vol. 52, pp. 509–536, 789–834.Google Scholar
[1980] Computability: An Introduction to Recursive Function Theory, Cambridge University Press.Google Scholar
[1972] Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem, Indagationes Mathematicae, vol. 34, pp. 381–392.Google Scholar
[1913] Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors, American Journal of Mathematics, vol. 35, pp. 413–422.Google Scholar
and [1974] Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen, Archiv für Mathematische Logik und Grundlagenforschung, vol. 16, pp. 49–66.Google Scholar
[1979] New kinds of realizability, Abstracts of the 6th International Congress of Logic, Methodology and Philosophy of Sciences, Hannover, Germany, pp. 20–24.Google Scholar
[1994] Normal Proofs in Set Theory, PhD thesis, Department of Computer Science, University of Göteborg.
[1972] Everywhere defined continuous functionals, Algebra i Logika, vol. 11, no. 6, pp. 656–665.Google Scholar
[1977] ModelC of partial continuous functionals, Logic colloquium 1976 ( and , editors), North-Holland, Amsterdam, pp. 455–467.Google Scholar
and [1992] Ordinal complexity of recursive definitions, Information and Computation, vol. 99, pp. 123–153.Google Scholar
and [1998] Hierarchies of provably recursive functions, Handbook of Proof Theory (, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam, pp. 149–207.Google Scholar
[1960] Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae, vol. XLIX, pp. 35–92.Google Scholar
[1962] Classifications of recursive functions by means of hierarchies, Transactions American Mathematical Society, vol. 104, pp. 101–122.Google Scholar
[1970] Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitioninism and proof theory ( and , editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 303–325.Google Scholar
[1982] Iterated inductive fixed point theories: applications to Hancock's conjecture, The Patras Symposium (, editor), North-Holland, Amsterdam, pp. 171–196.Google Scholar
[1992] Logics for termination and correctness of functional programs, Logic from Computer Science, Proceedings of a Workshop held November 13–17, 1989 (, editor), MSRI Publications, no. 21, Springer Verlag, Berlin, pp. 95–127.Google Scholar
[1996] Computation on abstract data types. The extensional approach, with an application to streams, Annals of Pure and Applied Logic, vol. 81, pp. 75–113.
, et al. [1986, 1990, 1995, 2002a, 2002b] Kurt Gödel Collected Works, Volume I–V, Oxford University Press.Google Scholar
and [2000] The unfolding of non-finitist arithmetic, Annals of Pure and Applied Logic, vol. 104, pp. 75–96.Google Scholar
and [2010] Unfolding finitist arithmetic, Review of Symbolic Logic, vol. 3, pp. 665–689.Google Scholar
, , , and [1987] A syntactic theory of sequential control, Theoretical Computer Science, vol. 52, pp. 205–237.Google Scholar
and [1992] The revised report on the syntactic theory of sequential control and state, Theoretical Computer Science, vol. 102, pp. 235–271.Google Scholar
[1999] A semantic account of type-directed partial evaluation, Principles and Practice of Declarative Programming 1999, Lecture Notes in Computer Science, vol. 1702, Springer Verlag, Berlin, pp. 378–395.Google Scholar
[1970] Iterated inductive definitions and ∑12-AC, Intuitioninism and proof theory ( and , editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 435–442.Google Scholar
[1978] Classically and intuitionistically provably recursive functions, Higher Set Theory ( and , editors), Lecture Notes in Mathematics, vol. 669, Springer Verlag, Berlin, pp. 21–28.Google Scholar
[1981] Independence results in finite graph theory, Unpublished manuscripts, Ohio State University, 76 pages.Google Scholar
[1982] Beyond Kruskal's theorem I–III, Unpublished manuscripts, Ohio State University, 48 pages.Google Scholar
, , and [1987] The metamathematics of the graph minor theorem, Logic and Combinatorics (, editor), Contemporary Mathematics, vol. 65, American Mathematical Society, pp. 229–261.Google Scholar
and [1995] Elementary descent recursion and proof theory, Annals of Pure and Applied Logic, vol. 71, pp. 1–45.Google Scholar
[1935] Untersuchungen über das logische Schließen I, II, Mathematische Zeitschrift, vol. 39, pp. 176–210, 405–431.Google Scholar
[1936] Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112, pp. 493–565.Google Scholar
[1943] Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie, Mathematische Annalen, vol. 119, pp. 140–161.Google Scholar
and [2008] General logical metatheorems for functional analysis, Transactions of the American Mathematical Society, vol. 360, pp. 2615–2660.Google Scholar
[1971] Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proceedings of the Second Scandinavian Logic Symposium (, editor), North-Holland, Amsterdam, pp. 63–92.Google Scholar
[1981] Π12-logic. Part I: Dilators, Annals of Mathematical Logic, vol. 21, pp. 75–219.Google Scholar
[1931] Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, vol. 38, pp. 173–198.Google Scholar
[1958] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts, Dialectica, vol. 12, pp. 280–287.Google Scholar
[1944] On the restricted ordinal theorem, The Journal of Symbolic Logic, vol. 9, pp. 33–41.Google Scholar
, , and [1990] Ramsey Theory, second ed., Discrete Mathematics and Optimization, Wiley Interscience.Google Scholar
[1990] A formulae-as-types notion of control, Conference Record of the Seventeenth Annual ACMSymposium on Principles of Programming Languages, pp. 47–58.Google Scholar
[1987] A typed lambda calculus with categorical type constructions, Category Theory and Computer Science (, , and , editors), Lecture Notes in Computer Science, vol. 283, Springer Verlag, Berlin, pp. 140–157.Google Scholar
and [1993] Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer Verlag, Berlin.Google Scholar
and [1999] Complexity of primitive recursion, Computational Logic ( and , editors), NATO ASISeries F, Springer Verlag, Berlin, pp. 273–300.Google Scholar
[1904] A theorem concerning the infinite cardinal numbers, Quaterly Journal of Mathematics, vol. 35, pp. 87–94.Google Scholar
and [1996] Axioms for subrecursion theories, Computability, Enumerability, Unsolvability. Directions in recursion theory (, , and , editors), London Mathematical Society Lecture Notes Series, vol. 224, Cambridge University Press, pp. 123–138.Google Scholar
[2006] Feasible Programs from (Non-Constructive) Proofs by the Light (Monotone) Dialectica Interpretation, PhD thesis, Ecole Polytechnique Paris and LMU München.
and [2010] Light Dialectica revisited, Annals of Pure and Applied Logic, vol. 161, pp. 1379–1389.Google Scholar
[1999] Linear types and non-size-increasing polynomial time computation, Proceedings 14'th Symposium on Logic in Computer Science (LICS '99), pp. 464–473.Google Scholar
[2000] Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol. 104, pp. 113–166.Google Scholar
[1970] Assignment of ordinals to terms for primitive recursive functionals of finite type, Intuitioninism and proof theory ( and , editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 443–458.Google Scholar
[1980] The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism ( and , editors), Academic Press, pp. 479–490.Google Scholar
[2010] On the computional content of choice axioms, Master's thesis, Mathematisches Institut der Universität München.
[2000] A note on the Gödel–Gentzen translation, Mathematical Logic Quarterly, vol. 46, pp. 135–137.Google Scholar
[1986] Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibliopolis, Naples.Google Scholar
, , , and [1999] The proof-theoretic analysis of transfinitely iterated fixed point theories, The Journal of Symbolic Logic, vol. 64, no. 1, pp. 53–67.Google Scholar
[1934] On the rules of supposition in formal logic (Polish), Studia Logica (old series), vol. 1, pp. 5–32, translated in Polish Logic 1920–39 (, editor), Clarendon Press, Oxford 1967.Google Scholar
[2005] Finite trees as ordinals, New Computational Paradigms; Proceedings of CiE 2005 (, , and , editors), Lecture Notes in Computer Science, vol. 3526, Springer Verlag, Berlin, pp. 211–220.Google Scholar
and [2003] Short proofs of normalisation for the simply-typed λ-calculus, permutative conversions and Gödel's T, Archive for Mathematical Logic, vol. 42, pp. 59–87.Google Scholar
[1972] Ramsey's theorem and recursion theory, The Journal of Symbolic Logic, vol. 37, pp. 268–280.Google Scholar
[1937] Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, vol. 4, pp. 119–136.Google Scholar
[2001] Finite type arithmetic, Master's thesis, University of Roskilde.
[1993] On Wainer's notation for a minimal subrecursive inaccessible ordinal, Mathematical Logic Quarterly, vol. 39, pp. 217–227.Google Scholar
[1943] Ein einfaches Beispiel für ein unentscheidbares Problem (Hungarian, with German summary), Mat. Fiz. Lapok, vol. 50, pp. 1–23.Google Scholar
and [1981] Rapidly growing Ramsey furnctions, Annals of Mathematics (2), vol. 113, pp. 267–314.Google Scholar
, , and [1970] Intuitioninism and Proof Theory, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.Google Scholar
and [1982] Accessible independence results for Peano arithmetic, Bulletin of the American Mathematical Society, vol. 113, pp. 285–293.Google Scholar
[1958] Extension of an effectively generated class of functions by enumeration, Colloquium Mathematicum, vol. 6, pp. 67–78.
[1996] Analysing proofs in analysis, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993) (, , , and , editors), Oxford University Press, pp. 225–260.Google Scholar
[2005] Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357, pp. 89–128.CrossRefGoogle Scholar
[2008] Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Verlag, Berlin.Google Scholar
and [2003] Mann iterates of directionally nonexpansive mappings in hyperbolic spaces, Abstracts in Applied Analysis, vol. 8, pp. 449–477.Google Scholar
and [2003a] Proof mining: a systematic way of analysing proofs in mathematics, Proceedings of the Steklov Institute of Mathematics, vol. 242, pp. 136–164.Google Scholar
and [2003b] Proof mining in L1 approximation, Annals of Pure and Applied Logic, vol. 121, pp. 1–38.Google Scholar
[1925] On the principle of the excluded middle (Russian), Matematicheskij Sbornik. Akademiya Nauk SSSRi Moskovskoe Matematicheskoe Obshchestvo, vol. 32, pp. 646–667, translated in FromFrege toGödel. A Source Book in Mathematical Logic 1879–1931 (, editor), Harvard University Press, Cambridge, MA., 1967, pp. 414–437.Google Scholar
[1932] Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, vol. 35, pp. 58–65.
[1951] On the interpretation of non-finitist proofs I, The Journal of Symbolic Logic, vol. 16, pp. 241–267.Google Scholar
[1952] On the interpretation of non-finitist proofs II, The Journal of Symbolic Logic, vol. 17, pp. 43–58.Google Scholar
[1959] Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics (, editor), North-Holland, Amsterdam, pp. 101–128.Google Scholar
[1963] Generalized inductive definitions, Reports for the seminar on foundations of analysis, vol. I, Stanford University, mimeographed.Google Scholar
and [1968] Reflection principles and their use for establishing the complexity of axiomatic systems, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 14, pp. 97–142.Google Scholar
[1965] Semantical analysis of intuitionistic logic I, Formal Systems and Recursive Functions ( and , editors), North-Holland, Amsterdam, pp. 93–130.Google Scholar
and [1997] Total objects in inductively defined types, Archive for Mathematical Logic, vol. 36, no. 6, pp. 405–436.Google Scholar
[1994] Classical logic, storage operators and second-order lambdacalculus, Annals of Pure and Applied Logic, vol. 68, pp. 53–78.Google Scholar
[1960] Well-quasi-orderings, the tree theorem and Vaszonyi's conjecture, Transactions of the American Mathematical Society, vol. 95, pp. 210–255.Google Scholar
and [1991] Using information systems to solve recursive domain equations, Information and Computation, vol. 91, pp. 232–258.Google Scholar
[1985] Syntactic translations and provably recursive functions, The Journal of Symbolic Logic, vol. 50, no. 3, pp. 682–688.Google Scholar
[1994] Predicative recurrence in finite type, Logical Foundations of Computer Science ( and , editors), Lecture Notes in Computer Science, vol. 813, pp. 227–239.Google Scholar
[1995a] Intrinsic theories and computational complexity, Logic and Computational Complexity, International Workshop LCC'94, Indianapolis, IN, USA, October 1994 (, editor), Lecture Notes in Computer Science, vol. 960, Springer Verlag, Berlin, pp. 177–194.Google Scholar
[1995b] Ramified recurrence and computational complexity I: Word recurrence and poly-time, Feasible Mathematics II ( and , editors), Birkhäuser, Boston, pp. 320–343.Google Scholar
and [1993] Lambda calculus characterization of poly-time, Fundamenta Informaticae, vol. 19, pp. 167–184.Google Scholar
[1960] A theorem on general recursive functions, Proceedings American Mathematical Society, vol. 11, pp. 184–187.Google Scholar
[1955] Solution of a problem of Leon Henkin, The Journal of Symbolic Logic, vol. 20, pp. 115–118.Google Scholar
and [1970] Hierarchies of number theoretic functions I, II, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 39–51, 97–113.Google Scholar
[2001] Actual arithmetic and feasibility, 15th International workshop, Computer Science Logic, CSL '01 (, editor), Lecture Notes in Computer Science, vol. 2142, Springer Verlag, Berlin, pp. 115–139.Google Scholar
[1971] Hauptsatz for the intuitionistic theory of iterated inductive definitions, Proceedings of the Second Scandinavian Logic Symposium (, editor), North-Holland, Amsterdam, pp. 179–216.Google Scholar
[1972] Infinite terms and a system of natural deduction, Compositio Mathematica, vol. 24, no. 1, pp. 93–103.Google Scholar
[1983] The domain interpretation of type theory, Talk at the workshop on semantics of programming languages, Chalmers University,Göteborg, August.
[1963] A basis for a mathematical theory of computation, Computer Programs and Formal Methods, North-Holland, Amsterdam, pp. 33–70.Google Scholar
[1973] Quantifier-free and one-quantifier systems, Journal of Soviet Mathematics, vol. 1, pp. 71–84.Google Scholar
[1978] Finite investigations of transfinite derivations, Journal of Soviet Mathematics, vol. 10, pp. 548–596, translated from Zap. Nauchn. Semin. LOMI, vol. 49 (1975).Google Scholar
[2000] A Short Introduction to Intuitionistic Logic, Kluwer Academic/Plenum Publishers, New York.Google Scholar
[2001] The implicit calculus of constructions. Extending pure type systems with an intersection type binder and subtyping, Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA '01) (Samson Abramsky, editor), Lecture Notes in Computer Science, vol. 2044, Springer Verlag, Berlin, pp. 344–359.
and [1984] An early program proof by Alan Turing, Annals of the History of Computing, vol. 6, pp. 139–143.Google Scholar
[1997] The logic of functional recursion, Logic and Scientific Methods. Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995 (, , , and , editors), Synthese Library, vol. 259, Kluwer Academic Publishers, Dordrecht, Boston, London, pp. 179–208.Google Scholar
[1990] Extracting constructive content from classical proofs, Technical Report 90–1151, Dep. of Comp. Science, Cornell Univ., Ithaca, NewYork, PhD thesis.
[1953] A stumbling block in constructive mathematics (abstract), The Journal of Symbolic Logic, vol. 18, p. 190.Google Scholar
[1942] On theories with a combinatorial definition of “equivalence”, Annals of Mathematics, vol. 43, no. 2, pp. 223–243.Google Scholar
[2000] Computability over the partial continuous functionals, The Journal of Symbolic Logic, vol. 65, no. 3, pp. 1133–1142.Google Scholar
[2006] Computing with functionals – computability theory or computer science?, The Bulletin of Symbolic Logic, vol. 12, pp. 43–59.Google Scholar
[2001] Implicit Characterizations of Pspace, Proof Theory in Computer Science (, , and , editors), Lecture Bibliography 447 Notes in Computer Science, vol. 2183, Springer Verlag, Berlin, pp. 170–190.Google Scholar
[2006] Unifying functional interpretations, Notre Dame Journal of Formal Logic, vol. 47, pp. 262–290.Google Scholar
[1979] Lower bounds for increasing complexity of derivations after cut elimination, Zapiski Nauchnykh Seminarov Leningradskogo, vol. 88, pp. 137–161.Google Scholar
and [2005] Elementary arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 275–292.Google Scholar
[1992] λμ-calculus: an algorithmic interpretation of classical natural deduction, Proc. of Log. Prog. and Automatic Reasoning, St. Petersburg, Lecture Notes in Computer Science, vol. 624, Springer Verlag, Berlin, pp. 190–201.Google Scholar
[1980] A hierarchy of cuts in models of arithmetic, Model theory of algebra and arithmetic ( et al., editors), Lecture Notes in Mathematics, vol. 834, Springer Verlag, pp. 312–337.Google Scholar
and [1977] A mathematical incompleteness in Peano arithmetic, Handbook of Mathematical Logic (, editor), North-Holland, Amsterdam, pp. 1133–1142.Google Scholar
[1966] Ordinal recursion in partial systems of number theory (abstract), Notices of the American Mathematical Society, vol. 13, pp. 857–858.Google Scholar
[1972] On n-quantifier induction, The Journal of Symbolic Logic, vol. 37, no. 3, pp. 466–482.Google Scholar
[1973] Transfinite induction in subsystems of number theory (abstract), The Journal of Symbolic Logic, vol. 38, no. 3, pp. 544–545.Google Scholar
[1977] LCF considered as a programming language, Theoretical Computer Science, vol. 5, pp. 223–255.Google Scholar
[1978] Tω as a universal domain, Journal of Computer and System Sciences, vol. 17, pp. 209–236.Google Scholar
[1998] Subsystems of set theory and second order number theory, Handbook of Proof Theory (, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam, pp. 209–335.Google Scholar
[1965] Natural Deduction, Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy, vol. 3, Almqvist & Wiksell, Stockholm.
[2004] Getting results from programs extracted from classical proofs, Theoretical Computer Science, vol. 323, pp. 49–70.Google Scholar
[1930] On a problem of formal logic, Proceedings of the London Mathematical Society (2), vol. 30, pp. 264–286.Google Scholar
[1993] Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic, vol. 64, pp. 95–152.Google Scholar
[1978] Eine verallgemeinerte Funktionalinterpretation der Heyting Arithmetik endlicher Typen, PhD thesis, Universität Münster, Fachbereich Mathematik.
[1992] A proof-theoretic characterization of primitive recursive set functions, The Journal of Symbolic Logic, vol. 57, pp. 954–969.Google Scholar
[1993] How to develop proof-theoretic ordinal functions on the basis of admissible sets, Mathematical Logic Quarterly, vol. 39, pp. 47–54.Google Scholar
[1999] The realm of ordinal analysis, Sets and Proofs: Logic Colloquium '97 ( and , editors), London Mathematical Society Lecture Notes, vol. 258, Cambridge University Press, pp. 219–279.Google Scholar
[2005] Ordinal analysis of parameter free Π12-comprehension, Archive for Mathematical Logic, vol. 44, no. 3, pp. 263–362.Google Scholar
and [1993] Proof-theoretic investigations on Kruskal's theorem, Annals of Pure and Applied Logic, vol. 60, pp. 49–88.Google Scholar
and [2010] Decorating proofs, Proofs, Categories and Computations. Essays in honor of Grigori Mints ( and , editors), College Publications, pp. 171–188.Google Scholar
and [2010] Exploring the computational content of the Infinite Pigeonhole Principle, Journal of Logic and Computation, to appear.
[1965] Extensions of the constructive ordinals, The Journal of Symbolic Logic, vol. 30, no. 2, pp. 193–211.Google Scholar
[1963] Classes of predictably computable functions, Transactions American Mathematical Society, vol. 106, pp. 139–173.Google Scholar
[1965] Subrecursive Hierarchies, PhD thesis, Princeton University.
[1950] An essentially undecidable axiom system, Proceedings of the International Congress of Mathematicians (Cambridge 1950), vol. I, pp. 729–730.Google Scholar
[1968] Klassen rekursiver Funktionen, Proceedings of the Summer School in Logic, Lecture Notes in Mathematics, vol. 70, Springer Verlag, Berlin, pp. 159–222.Google Scholar
[1984] Subrecursion: Functions and Hierarchies, Oxford Logic Guides, vol. 9, Clarendon Press, Oxford.Google Scholar
[1936] Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, vol. 1, pp. 87–91.Google Scholar
[1953] Ordinal recursion, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 49, pp. 175–182.Google Scholar
[2000] Universal coalgebra: a theory of systems, Theoretical Computer Science, vol. 249, pp. 3–80.Google Scholar
[1976] Built-up systems of fundamental sequences and hierarchies of number-theoretic functions, Archiv für Mathematische Logik und Grundlagenforschung, vol. 18, pp. 47–53.Google Scholar
[1984] A natural extension of natural deduction, The Journal of Symbolic Logic, vol. 49, pp. 2184–1300.Google Scholar
[1951] Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie, Mathematische Annalen, vol. 122, pp. 369–389.Google Scholar
[1971] Eine Klassifikation der ε0-rekursiven Funktionen, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 17, pp. 61–74.Google Scholar
[1975] Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion, Logic Colloquium '73 ( and , editors), North-Holland, Amsterdam, pp. 279–303.Google Scholar
[1977] Proof theory: some applications of cut-elimination, Handbook of Mathematical Logic (, editor), Studies in Logic and the Foundations of Mathematics, vol. 90, North-Holland, Amsterdam, pp. 867–895.Google Scholar
[1992] Proofs as programs, Proof Theory (, , and , editors), Cambridge University Press, pp. 81–113.Google Scholar
[1996] Density and choice for total continuous functionals, Kreiseliana. About and Around Georg Kreisel (, editor), A.K. Peters, Wellesley, Massachusetts, pp. 335–362.Google Scholar
[2005] 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, vol. 11, no. 12, pp. 2086–2095.Google Scholar
[2006a] An arithmetic for polynomial-time computation, Theoretical Computer Science, vol. 357, pp. 202–214.Google Scholar
[2006b] Minlog, The Seventeen Provers of the World (, editor), Lecture Notes in Artificial Intelligence, vol. 3600, Springer Verlag, Berlin, pp. 151–157.Google Scholar
[2006c] Recursion on the partial continuous functionals, Logic Colloquium '05 (, , , and , editors), Lecture Notes in Logic, vol. 28, Association for Symbolic Logic, pp. 173–201.Google Scholar
[2008a] Dialectica interpretation of well-founded induction, Mathematical Logic Quarterly, vol. 54, no. 3, pp. 229–239.Google Scholar
[2008b] Realizability interpretation of proofs in constructive analysis, Theory of Computing Systems, vol. 43, no. 3, pp. 583–602.Google Scholar
and [2002] Feasible computation with higher types, Proof and System-Reliability ( and , editors), Proceedings NATO Advanced Study Institute, Marktoberdorf, 2001, Kluwer Academic Publisher, pp. 399–415.
and [1995] Ordinal bounds for programs, Feasible Mathematics II ( and , editors), Birkhäuser, Boston, pp. 387–406.Google Scholar
[1970] Outline of a mathematical theory of computation, Technical Monograph PRG-2, Oxford University Computing Laboratory.
[1982] Domains for denotational semantics, Automata, Languages and Programming ( and , editors), Lecture Notes in Computer Science, vol. 140, Springer Verlag, Berlin, pp. 577–613.Google Scholar
and [1963] Computability of recursive functions, Journal of the Association for Computing Machinery, vol. 10, pp. 217–255.Google Scholar
[1988] The realm of primitive recursion, Archive for Mathematical Logic, vol. 27, pp. 177–188.Google Scholar
[1985] Nonprovability of certain combinatorial properties of finite trees, Harvey Friedman's Research on the Foundations of Mathematics (, , , and , editors), North-Holland, Amsterdam, pp. 87–117.Google Scholar
[2009] Subsystems of Second Order Arithmetic, second ed., Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press.Google Scholar
[1987] Recursively Enumerable Sets and Degrees, Perspectives inMathematical Logic, Springer Verlag, Berlin.Google Scholar
[1992] Ordinal arithmetic in IΔ0, Arithmetic, Proof Theory and Computational Complexity ( and , editors), Oxford University Press.Google Scholar
[1995] Transfinite induction within Peano arithmetic, Annals of Pure and Applied Logic, vol. 76, pp. 231–289.Google Scholar
[2010] A Hierarchy of Ramified Theories Below Primitive Recursive Arithmetic, PhD thesis, Dept. of Pure Mathematics, Leeds University.
[1978] Bounds for proof-search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol. 15, pp. 225–287.Google Scholar
[1976] Interpretationen der Heyting-Arithmetik endlicher Typen, PhD thesis, Universität Münster, Fachbereich Mathematik.
, , and [1994] Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
and [1999] Computable rings and fields, Handbook of Computability Theory (, editor), North-Holland, Amsterdam, pp. 363–447.Google Scholar
[1997] Polynomial time operations in explicit mathematics, The Journal of Symbolic Logic, vol. 62, no. 2, pp. 575–594.Google Scholar
[2004] A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science, vol. 329, pp. 159–176.Google Scholar
and [2008] Primitive recursive selection functions for existential assertions over abstract algebras, Journal of Logic and Algebraic Programming, vol. 76, pp. 175–197.Google Scholar
[1968] Normal derivability in classical logic, The Syntax and Semantics of Infinitary Languages (, editor), Lecture Notes in Mathematics, vol. 72, Springer Verlag, Berlin, pp. 204–236.Google Scholar
[1971] Normal form theorem for bar recursive functions of finite type, Proceedings of the Second Scandinavian Logic Symposium (, editor), North-Holland, Amsterdam, pp. 353–367.Google Scholar
[1995] Parallel reductions in λ-calculus, Information and Computation, vol. 118, pp. 120–127.Google Scholar
[1967] Consistency proofs of subsystems of classical analysis, Annals of Mathematics, vol. 86, pp. 299–348.Google Scholar
[1936] Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, vol. 1, pp. 261–405.Google Scholar
[2009] Dialectica interpretation with fine computational control, Proc. 5th Conference on Computability in Europe, Lecture Notes in Computer Science, vol. 5635, Springer Verlag,/pn>, Berlin, pp. 467–477.Google Scholar
[1973] Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer Verlag, Berlin.Google Scholar
and [1988] Constructivism in Mathematics. An Introduction, Studies in Logic and the Foundations of Mathematics, vol. 121, 123, North-Holland, Amsterdam.Google Scholar
and [1992] Provable computable selection functions on abstract structures, Proof Theory (, , and , editors), Cambridge University Press, pp. 275–306.Google Scholar
and [2000] Computable functions and semicomputable sets on many-sorted algebras, Handbook of Logic in Computer Science, Vol. V (, , and , editors), Oxford University Press, pp. 317–523.Google Scholar
and [2006] Abstract versus concrete computability: the case of countable algebras, Logic Colloquium 2003 ( and , editors), ASL Lecture Notes in Logic, vol. 24, AK Peters, pp. 377–408.Google Scholar
[1995] Two different strong normalization proofs?, HOA 1995 (, , , and , editors), Lecture Notes in Computer Science, vol. 1074, Springer Verlag, Berlin, pp. 201–220.Google Scholar
and [1995] On normalisation, Computer Science Report CS-R9545 1995, Centrum voor Wiskunde en Informatica.
[2008] Gentzen's proof of normalization for natural deduction, The Bulletin of Symbolic Logic, vol. 14, no. 2, pp. 240–257.Google Scholar
[1970] A classification of the ordinal recursive functions, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 136–153.Google Scholar
[1972] Ordinal recursion, and a refinement of the extended Grzegorcyk hierarchy, The Journal of Symbolic Logic, vol. 38, pp. 281–292.Google Scholar
[1989] Slow growing versus fast growing, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 608–614.Google Scholar
[1999] Accessible recursive functions, The Bulletin of Symbolic Logic, vol. 5, no. 3, pp. 367–388.Google Scholar
[2010] Computing bounds from arithmetical proofs, Ways of Proof Theory: Festschrift for W. Pohlers (, editor), Ontos Verlag, pp. 459–476.Google Scholar
and [2005] Inductive definitions over a predicative arithmetic, Annals of Pure and Applied Logic, vol. 136, pp. 175–188.Google Scholar
[1995] Investigations on slow versus fast growing: how to majorize slow growing functions nontrivially by fast growing ones, Archive for Mathematical Logic, vol. 34, pp. 313–330.Google Scholar
[1996] How to characterize provably total functions by local predicativity, The Journal of Symbolic Logic, vol. 61, no. 1, pp. 52–69.Google Scholar
[1999] What makes a (pointwise) subrecursive hierarchy slow growing?, Sets and Proofs: Logic Colloquium '97 ( and , editors), London Mathematical Society Lecture Notes, vol. 258, Cambridge University Press, pp. 403–423.Google Scholar
[2004] A classification of rapidly growing Ramsey functions, Proceedings of the American Mathematical Society, vol. 132, pp. 553–561.Google Scholar
[2005] Analytic combinatorics, proof-theoretic ordinals, and phasetransitions for independence results, Annals of Pure and Applied Logic, vol. 136, pp. 189–218.Google Scholar
[2006] Classifying the provably total functions of PA, The Bulletin of Symbolic Logic, vol. 12, pp. 177–190.Google Scholar
[2007] Phase transition thresholds for some Friedman-style independence results, Mathematical Logic Quarterly, vol. 53, pp. 4–18.Google Scholar
[2004] Finitely Iterated Inductive Definitions over a Predicative Arithmetic, PhD thesis, Department of Pure Mathematics, Leeds University.
[1977] P.R.-regulated systems of notation and the subrecursive hierarchy equivalence property, Transactions of the American Mathematical Society, vol. 234, pp. 89–118.Google Scholar
[1973] Iterated inductivex1 definitions, trees and ordinals, Mathematical Investigation of Intuitionistic Arithmetic and Analysis (, editor), Lecture Notes in Mathematics, vol. 344, Springer Verlag, Berlin, pp. 392–453.Google Scholar