Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-24T09:55:08.192Z Has data issue: false hasContentIssue false

BIBLIOGRAPHY

Published online by Cambridge University Press:  05 January 2012

Helmut Schwichtenberg  and
Stanley S. Wainer
Helmut Schwichtenberg
Affiliation:
Ludwig-Maximilians-Universität Munchen
Stanley S. Wainer
Affiliation:
University of Leeds
Get access

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.
Image of the first page of this content. For PDF version, please use the ‘Save PDF’ preceeding this image.'
Type
Chapter
Information
Proofs and Computations , pp. 431 - 456
Publisher: Cambridge University Press
Print publication year: 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Andreas, Abel and Thorsten, Altenkirch [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
Samson, Abramsky [1991] Domain theory in logical form, Annals of Pure and Applied Logic, vol. 51, pp. 1–77.Google Scholar
Samson, Abramsky and Achim, Jung [1994] Domain theory, Handbook of Logic in Computer Science (S., Abramsky, D. M., Gabbay, and T. S. E., Maibaum, editors), vol. 3, Clarendon Press, pp. 1–168.
Wilhelm, Ackermann [1940] Zur Widerspruchsfreiheit der Zahlentheorie, Mathematische Annalen, vol. 117, pp. 162–194.Google Scholar
Peter, Aczel, Harold, Simmons, and Stanley S., Wainer [1992] Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, Cambridge University Press.
Klaus, Aehlig and Jan, Johannsen [2005] An elementary fragment of second-order lambda calculus, ACM Transactions on Computational Logic, vol. 6, pp. 468–480.Google Scholar
Roberto M., Amadio and Pierre-Louis, Curien [1998] Domains and Lambda-Calculi, Cambridge University Press.Google Scholar
Toshiyasu, Arai [1991] A slow growing analogue to Buchholz' proof, Annals of Pure and Applied Logic, vol. 54, pp. 101–120.Google Scholar
Toshiyasu, Arai [2000] Ordinal diagrams for recursively Mahlo universes, Archive for Mathematical Logic, vol. 39, no. 5, pp. 353–391.Google Scholar
Jeremy, Avigad [2000] Interpreting classical theories in constructive ones, The Journal of Symbolic Logic, vol. 65, no. 4, pp. 1785–1812.Google Scholar
Jeremy, Avigad and Rick, Sommer [1997] A model theoretic approach to ordinal analysis, The Bulletin of Symbolic Logic, vol. 3, pp. 17–52.Google Scholar
Franco, Barbanera and Stefano, Berardi [1993] Extracting constructive content from classical logic via control-like reductions, Typed Lambda Calculi and Applications (M., Bezem and J. F., Groote, editors), Lecture Notes in Computer Science, vol. 664, Springer|Verlag, Berlin, pp. 45–59.Google Scholar
Hendrik, Pieter Barendregt [1984] The Lambda Calculus, second ed., North-Holland, Amsterdam.Google Scholar
Henk, Barendregt, Mario, Coppo, and Mariangiola, Dezani-Ciancaglini [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
Arnold, Beckmann, Chris, Pollett, and Samuel R., Buss [2003] Ordinal notations and well-orderings in bounded arithmetic, Annals of Pure and Applied Logic, vol. 120, pp. 197–223.Google Scholar
Arnold, Beckmann and Andreas, Weiermann [1996] A term rewriting characterization of the polytime functions and related complexity classes, Archive for Mathematical Logic, vol. 36, pp. 11–30.Google Scholar
Lev D., Beklemishev [2003] Proof-theoretic analysis of iterated reflection, Archive for Mathematical Logic, vol. 42, no. 6, pp. 515–552.Google Scholar
Stephen, Bellantoni and Stephen, Cook [1992] A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol. 2, pp. 97–110.Google Scholar
Stephen, Bellantoni and Martin, Hofmann [2002] A new “feasible” arithmetic, The Journal of Symbolic Logic, vol. 67, no. 1, pp. 104–116.Google Scholar
Ulrich, Berger, Wilfried, Buchholz, and Helmut, Schwichtenberg [2000] Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol. 104, pp. 17–30.Google Scholar
Holger, Benl [1998] Konstruktive Interpretation induktiver Definitionen, Master's thesis, Mathematisches Institut der Universität München.
Ulrich, Berger [1993a] Program extraction from normalization proofs, Typed Lambda Calculi and Applications (M., Bezem and J. F., Groote, editors), Lecture Notes in Computer Science, vol. 664, Springer Verlag, Berlin, pp. 91–106.Google Scholar
Ulrich, Berger [1993b] Total sets and objects in domain theory, Annals of Pure and Applied Logic, vol. 60, pp. 91–117.Google Scholar
Ulrich, Berger [2005a] Continuous semantics for strong normalization, Proceedings CiE 2005, Lecture Notes in Computer Science, vol. 3526, pp. 23–34.Google Scholar
Ulrich, Berger [2005b] Uniform Heyting arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 125–148.Google Scholar
Ulrich, Berger [2009] From coinductive proofs to exact real arithmetic, Computer Science Logic (E., Grädel and R., Kahle, editors), Lecture Notes in Computer Science, Springer Verlag, Berlin, pp. 132–146.Google Scholar
Ulrich, Berger, Stefan, Berghofer, Pierre, Letouzey, and Helmut, Schwichtenberg [2006] Program extraction from normalization proofs, Studia Logica, vol. 82, pp. 27–51.Google Scholar
Ulrich, Berger, Wilfried, Buchholz, and Helmut, Schwichtenberg [2002] Refined program extraction from classical proofs, Annals of Pure and Applied Logic, vol. 114, pp. 3–25.Google Scholar
Ulrich, Berger, Matthias, Eberl, and Helmut, Schwichtenberg [2003] Term rewriting for normalization by evaluation, Information and Computation, vol. 183, pp. 19–42.Google Scholar
Ulrich, Berger and Helmut, Schwichtenberg [1991] An inverse of the evaluation functional for typed λ-calculus, Proceedings 6'th Symposium on Logic in Computer Science (LICS'91) (R., Vemuri, editor), IEEE Computer Society Press, Los Alamitos, pp. 203–211.Google Scholar
Ulrich, Berger, Helmut, Schwichtenberg, and Monika, Seisenberger [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
Evert, Willem Beth [1956] Semantic construction of intuitionistic logic, Medelingen de KNAW N.S., vol. 19, no. 11.Google Scholar
Evert, Willem Beth [1959] The Foundations of Mathematics, North-Holland, Amsterdam.Google Scholar
Marc, Bezem and Vim, Veldman [1993] Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics, Journal of the London Mathematical Society, vol. 47, pp. 193–211.Google Scholar
Frédéric, Blanqui, Jean-Pierre, Jouannaud, and Mitsuhiro, Okada [1999] The Calculus of Algebraic Constructions, RTA '99, Lecture Notes in Computer Science, vol. 1631.Google Scholar
Egon, Börger, Erich, Grädel, and Yuri, Gurevich [1997] The Classical Decision Problem, Perspectives in Mathematical Logic, Springer Verlag, Berlin.Google Scholar
Alan, Borodin and Robert L., Constable [1971] Subrecursive programming languages II: on program size, Journal of Computer and System Sciences, vol. 5, pp. 315–334.Google Scholar
Andrey, Bovykin [2009] Brief introduction to unprovability, Logic colloquium 2006, Lecture Notes in Logic, Association for Symbolic Logic and Cambridge University Press, pp. 38–64.
Wilfried, Buchholz [1980] Three contributions to the conference on recent advances in proof theory, Handwritten notes.
Wilfried, Buchholz [1987] An independence result for –CA+BI, Annals of Pure and Applied Logic, vol. 33, no. 2, pp. 131–155.Google Scholar
Wilfried, Buchholz, Adam, Cichon, and Andreas, Weiermann [1994] A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 40, pp. 273–286.Google Scholar
Wilfried, Buchholz, Solomon, Feferman, Wolfram, Pohlers, and Wilfried, Sieg [1981] Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Mathematics, vol. 897, Springer|Verlag, Berlin, Berlin.Google Scholar
Wilfried, Buchholz and Wolfram, Pohlers [1978] Provable wellorderings of formal theories for transfinitely iterated inductive definitions, The Journal of Symbolic Logic, vol. 43, pp. 118–125.Google Scholar
Wilfried, Buchholz and Stanley S., Wainer [1987] Provably computable functions and the fast growing hierarchy, Logic and Combinatorics (S. G., Simpson, editor), Contemporary Mathematics, vol. 65, American Mathematical Society, pp. 179–198.Google Scholar
Samuel R., Buss [1986] Bounded Arithmetic, Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli.Google Scholar
Samuel R., Buss [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 (D., Prawitz, B., Skyrms, and D., Westerstahl, editors), North-Holland, Amsterdam, pp. 29–68.Google Scholar
Samuel R., Buss [1998a] First order proof theory of arithmetic, Handbook of Proof Theory (S., Buss, editor), North-Holland, Amsterdam, pp. 79–147.Google Scholar
Samuel R., Buss [1998b] Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam.Google Scholar
N., Çagman, G. E., Ostrin, and S. S., Wainer [2000] Proof theoretic complexity of low subrecursive classes, Foundations of Secure Computation (F. L., Bauer and R., Steinbrüggen, editors), NATO Science Series F, vol. 175, IOS Press, pp. 249–285.Google Scholar
Andrea, Cantini [2002] Polytime, combinatory logic and positive safe induction, Archive for Mathematical Logic, vol. 41, no. 2, pp. 169–189.Google Scholar
Timothy J., Carlson [2001] Elementary patterns of resemblance, Annals of Pure and Applied Logic, vol. 108, pp. 19–77.Google Scholar
Victor P., Chernov [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
Luca, Chiarabini [2009] Program Development by Proof Transformation, PhD thesis, Fakultät f ür Mathematik, Informatik und Statistik der LMU,München.
Alonzo, Church [1936] A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1, pp. 40–41, Correction, ibid., pp. 101–102.Google Scholar
Adam, Cichon [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
John P., Cleave [1963] A hierarchy of primitive recursive functions, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 9, pp. 331–345.Google Scholar
Peter, Clote and Gaisi, Takeuti [1995] First order bounded arithmetic and small boolean circuit complexity classes, Feasible Mathematics II (P., Clote and J., Remmel, editors), Birkhäuser, Boston, pp. 154–218.Google Scholar
Alan, Cobham [1965] The intrinsic computational difficulty of functions, Logic, Methodology and Philosophy of Science II (Y., Bar-Hillel, editor), North-Holland, Amsterdam, pp. 24–30.Google Scholar
Robert L., Constable [1972] Subrecursive programming languages I: efficiency and program structure, Journal of the ACM, vol. 19, pp. 526–568.Google Scholar
Robert L., Constable and Chetan, Murthy [1991] Finding computational content in classical proofs, Logical Frameworks (G., Huet and G., Plotkin, editors), Cambridge University Press, pp. 341–362.Google Scholar
Stephen A., Cook and Bruce M., Kapron [1990] Characterizations of the basic feasible functionals of finite type, Feasible Mathematics (S., Buss and P., Scott, editors), Birkhäuser, pp. 71–96.Google Scholar
S. Barry, Cooper [2003] Computability Theory, Shapman Hall/CRC.Google Scholar
,Coq Development Team [2009] The Coq Proof Assistant Reference Manual – Version 8.2, Inria.
Thierry, Coquand and Martin, Hofmann [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
Thierry, Coquand and Hendrik, Persson [1999] Gröbner bases in type theory, Types for Proofs and Programs (T., Altenkirch, W., Naraschewski, and B., Reus, editors), Lecture Notes in Computer Science, vol. 1657, Springer Verlag, Berlin.Google Scholar
Thierry, Coquand, Giovanni, Sambin, Jan, Smith, and Silvio, Valentini [2003] Inductively generated formal topologies, Annals of Pure and Applied Logic, vol. 124, pp. 71–106.Google Scholar
Thierry, Coquand and Arnaud, Spiwack [2006] A proof of strong normalisation using domain theory, Proceedings LICS 2006, pp. 307–316.Google Scholar
Haskell B., Curry [1930] Grundlagen der kombinatorischen Logik, American Journal of Mathematics, vol. 52, pp. 509–536, 789–834.Google Scholar
Nigel J., Cutland [1980] Computability: An Introduction to Recursive Function Theory, Cambridge University Press.Google Scholar
Nicolaas G., de Bruijn [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
Leonard E., Dickson [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
Justus, Diller and W., Nahm [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
Albert, Dragalin [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
Jan, Ekman [1994] Normal Proofs in Set Theory, PhD thesis, Department of Computer Science, University of Göteborg.
Yuri L., Ershov [1972] Everywhere defined continuous functionals, Algebra i Logika, vol. 11, no. 6, pp. 656–665.Google Scholar
Yuri L., Ershov [1977] ModelC of partial continuous functionals, Logic colloquium 1976 (R., Gandy and M., Hyland, editors), North-Holland, Amsterdam, pp. 455–467.Google Scholar
Matthew V. H., Fairtlough and Stanley S., Wainer [1992] Ordinal complexity of recursive definitions, Information and Computation, vol. 99, pp. 123–153.Google Scholar
Matthew V. H., Fairtlough and Stanley S., Wainer [1998] Hierarchies of provably recursive functions, Handbook of Proof Theory (S., Buss, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam, pp. 149–207.Google Scholar
Solomon, Feferman [1960] Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae, vol. XLIX, pp. 35–92.Google Scholar
Solomon, Feferman [1962] Classifications of recursive functions by means of hierarchies, Transactions American Mathematical Society, vol. 104, pp. 101–122.Google Scholar
Solomon, Feferman [1970] Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitioninism and proof theory (J., MyhillA., Kino and R. E., Vesley, editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 303–325.Google Scholar
Solomon, Feferman [1982] Iterated inductive fixed point theories: applications to Hancock's conjecture, The Patras Symposium (G., Metakides, editor), North-Holland, Amsterdam, pp. 171–196.Google Scholar
Solomon, Feferman [1992] Logics for termination and correctness of functional programs, Logic from Computer Science, Proceedings of a Workshop held November 13–17, 1989 (Y. N., Moschovakis, editor), MSRI Publications, no. 21, Springer Verlag, Berlin, pp. 95–127.Google Scholar
Solomon, Feferman [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.
Solomon, Feferman, John W., Dawson et al. [1986, 1990, 1995, 2002a, 2002b] Kurt Gödel Collected Works, Volume I–V, Oxford University Press.Google Scholar
Solomon, Feferman and Thomas, Strahm [2000] The unfolding of non-finitist arithmetic, Annals of Pure and Applied Logic, vol. 104, pp. 75–96.Google Scholar
Solomon, Feferman and Thomas, Strahm [2010] Unfolding finitist arithmetic, Review of Symbolic Logic, vol. 3, pp. 665–689.Google Scholar
Matthias, Felleisen, Daniel P., Friedman, E., Kohlbecker, and B. F., Duba [1987] A syntactic theory of sequential control, Theoretical Computer Science, vol. 52, pp. 205–237.Google Scholar
Matthias, Felleisen and R., Hieb [1992] The revised report on the syntactic theory of sequential control and state, Theoretical Computer Science, vol. 102, pp. 235–271.Google Scholar
Andrzej, Filinski [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
Harvey, Friedman [1970] Iterated inductive definitions and ∑12-AC, Intuitioninism and proof theory (J., MyhillA., Kino and R. E., Vesley, editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 435–442.Google Scholar
Harvey, Friedman [1978] Classically and intuitionistically provably recursive functions, Higher Set Theory (D. S., Scott and G. H., Müller, editors), Lecture Notes in Mathematics, vol. 669, Springer Verlag, Berlin, pp. 21–28.Google Scholar
Harvey, Friedman [1981] Independence results in finite graph theory, Unpublished manuscripts, Ohio State University, 76 pages.Google Scholar
Harvey, Friedman [1982] Beyond Kruskal's theorem I–III, Unpublished manuscripts, Ohio State University, 48 pages.Google Scholar
Harvey, Friedman, Neil, Robertson, and Paul, Seymour [1987] The metamathematics of the graph minor theorem, Logic and Combinatorics (S. G., Simpson, editor), Contemporary Mathematics, vol. 65, American Mathematical Society, pp. 229–261.Google Scholar
Harvey, Friedman and Michael, Sheard [1995] Elementary descent recursion and proof theory, Annals of Pure and Applied Logic, vol. 71, pp. 1–45.Google Scholar
Gerhard, Gentzen [1935] Untersuchungen über das logische Schließen I, II, Mathematische Zeitschrift, vol. 39, pp. 176–210, 405–431.Google Scholar
Gerhard, Gentzen [1936] Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112, pp. 493–565.Google Scholar
Gerhard, Gentzen [1943] Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie, Mathematische Annalen, vol. 119, pp. 140–161.Google Scholar
Philipp, Gerhardy and Ulrich, Kohlenbach [2008] General logical metatheorems for functional analysis, Transactions of the American Mathematical Society, vol. 360, pp. 2615–2660.Google Scholar
Jean-Yves, Girard [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 (J. E., Fenstad, editor), North-Holland, Amsterdam, pp. 63–92.Google Scholar
Jean-Yves, Girard [1981] Π12-logic. Part I: Dilators, Annals of Mathematical Logic, vol. 21, pp. 75–219.Google Scholar
Jean-Yves, Girard [1987] Proof Theory and Logical Complexity, Bibliopolis, Napoli.Google Scholar
Jean-Yves, Girard [1998] Light linear logic, Information and Computation, vol. 143, pp. 175–204.Google Scholar
Kurt, Gödel [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
Kurt, Gödel [1958] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts, Dialectica, vol. 12, pp. 280–287.Google Scholar
Ruben L., Goodstein [1944] On the restricted ordinal theorem, The Journal of Symbolic Logic, vol. 9, pp. 33–41.Google Scholar
Ronald, Graham, Bruce, Rothschild, and Joel, Spencer [1990] Ramsey Theory, second ed., Discrete Mathematics and Optimization, Wiley Interscience.Google Scholar
Timothy G., Griffin [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
Andrzey, Grzegorczyk [1953] Some Classes of Recursive Functions, Rozprawy Matematyczne, Warszawa.Google Scholar
Tatsuya, Hagino [1987] A typed lambda calculus with categorical type constructions, Category Theory and Computer Science (D. H., Pitt, A., Poigné, and D. E., Rydeheard, editors), Lecture Notes in Computer Science, vol. 283, Springer Verlag, Berlin, pp. 140–157.Google Scholar
Petr, Hájek and Pavel, Pudlák [1993] Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer Verlag, Berlin.Google Scholar
William G., Handley and Stanley S., Wainer [1999] Complexity of primitive recursion, Computational Logic (U., Berger and H., Schwichtenberg, editors), NATO ASISeries F, Springer Verlag, Berlin, pp. 273–300.Google Scholar
Godfrey H., Hardy [1904] A theorem concerning the infinite cardinal numbers, Quaterly Journal of Mathematics, vol. 35, pp. 87–94.Google Scholar
Andrew J., Heaton and Stanley S., Wainer [1996] Axioms for subrecursion theories, Computability, Enumerability, Unsolvability. Directions in recursion theory (S. B., Cooper, T. A., Slaman, and S. S., Wainer, editors), London Mathematical Society Lecture Notes Series, vol. 224, Cambridge University Press, pp. 123–138.Google Scholar
Mircea Dan, Hernest [2006] Feasible Programs from (Non-Constructive) Proofs by the Light (Monotone) Dialectica Interpretation, PhD thesis, Ecole Polytechnique Paris and LMU München.
Mircea Dan, Hernest and Trifon, Trifonov [2010] Light Dialectica revisited, Annals of Pure and Applied Logic, vol. 161, pp. 1379–1389.Google Scholar
Arend, Heyting [1959] Constructivity in mathematics, North-Holland, Amsterdam.Google Scholar
David, Hilbert and Paul, Bernays [1939] Grundlagen der Mathematik, vol. II, Springer Verlag, Berlin.Google Scholar
Martin, Hofmann [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
Martin, Hofmann [2000] Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol. 104, pp. 113–166.Google Scholar
William A., Howard [1970] Assignment of ordinals to terms for primitive recursive functionals of finite type, Intuitioninism and proof theory (J., MyhillA., Kino and R. E., Vesley, editors), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp. 443–458.Google Scholar
William A., Howard [1980] The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (J. P., Seldin and J. R., Hindley, editors), Academic Press, pp. 479–490.Google Scholar
Simon, Huber [2010] On the computional content of choice axioms, Master's thesis, Mathematisches Institut der Universität München.
Hajime, Ishihara [2000] A note on the Gödel–Gentzen translation, Mathematical Logic Quarterly, vol. 46, pp. 135–137.Google Scholar
Gerhard, Jäger [1986] Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibliopolis, Naples.Google Scholar
Gerhard, Jäger, Reinhard, Kahle, Anton, Setzer, and Thomas, Strahm [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
Stanislaw, Jáskowski [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 (S., McCall, editor), Clarendon Press, Oxford 1967.Google Scholar
Herman R., Jervell [2005] Finite trees as ordinals, New Computational Paradigms; Proceedings of CiE 2005 (S. B., Cooper, B., Löwe, and L., Torenvliet, editors), Lecture Notes in Computer Science, vol. 3526, Springer Verlag, Berlin, pp. 211–220.Google Scholar
Felix, Joachimski and Ralph, Matthes [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
Carl G., Jockusch [1972] Ramsey's theorem and recursion theory, The Journal of Symbolic Logic, vol. 37, pp. 268–280.Google Scholar
Ingebrigt, Johansson [1937] Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, vol. 4, pp. 119–136.Google Scholar
Klaus Frovin, Jørgensen [2001] Finite type arithmetic, Master's thesis, University of Roskilde.
Noriya, Kadota [1993] On Wainer's notation for a minimal subrecursive inaccessible ordinal, Mathematical Logic Quarterly, vol. 39, pp. 217–227.Google Scholar
Lazlo, Kalmár [1943] Ein einfaches Beispiel für ein unentscheidbares Problem (Hungarian, with German summary), Mat. Fiz. Lapok, vol. 50, pp. 1–23.Google Scholar
Jussi, Ketonen and Robert M., Solovay [1981] Rapidly growing Ramsey furnctions, Annals of Mathematics (2), vol. 113, pp. 267–314.Google Scholar
Akiko, Kino, John, Myhill, and Richard E., Vesley [1970] Intuitioninism and Proof Theory, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.Google Scholar
Laurie A. S., Kirby and Jeff B., Paris [1982] Accessible independence results for Peano arithmetic, Bulletin of the American Mathematical Society, vol. 113, pp. 285–293.Google Scholar
Stephen C., Kleene [1952] Introduction to Metamathematics, D., van Nostrand, New York.Google Scholar
Stephen C., Kleene [1958] Extension of an effectively generated class of functions by enumeration, Colloquium Mathematicum, vol. 6, pp. 67–78.
Ulrich, Kohlenbach [1996] Analysing proofs in analysis, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993) (W., Hodges, M., Hyland, C., Steinhorn, and J., Truss, editors), Oxford University Press, pp. 225–260.Google Scholar
Ulrich, Kohlenbach [2005] Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357, pp. 89–128.CrossRefGoogle Scholar
Ulrich, Kohlenbach [2008] Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Verlag, Berlin.Google Scholar
Ulrich, Kohlenbach and Laurentin, Leustean [2003] Mann iterates of directionally nonexpansive mappings in hyperbolic spaces, Abstracts in Applied Analysis, vol. 8, pp. 449–477.Google Scholar
Ulrich, Kohlenbach and Paulo, Oliva [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
Ulrich, Kohlenbach and Paulo, Oliva [2003b] Proof mining in L1 approximation, Annals of Pure and Applied Logic, vol. 121, pp. 1–38.Google Scholar
Andrey N., Kolmogorov [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 (J., van Heijenoort, editor), Harvard University Press, Cambridge, MA., 1967, pp. 414–437.Google Scholar
Andrey N., Kolmogorov [1932] Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, vol. 35, pp. 58–65.
Georg, Kreisel [1951] On the interpretation of non-finitist proofs I, The Journal of Symbolic Logic, vol. 16, pp. 241–267.Google Scholar
Georg, Kreisel [1952] On the interpretation of non-finitist proofs II, The Journal of Symbolic Logic, vol. 17, pp. 43–58.Google Scholar
Georg, Kreisel [1959] Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics (Arend, Heyting, editor), North-Holland, Amsterdam, pp. 101–128.Google Scholar
Georg, Kreisel [1963] Generalized inductive definitions, Reports for the seminar on foundations of analysis, vol. I, Stanford University, mimeographed.Google Scholar
Georg, Kreisel and Azriel, Lévy [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
Saul A., Kripke [1965] Semantical analysis of intuitionistic logic I, Formal Systems and Recursive Functions (J., Crossley and M., Dummett, editors), North-Holland, Amsterdam, pp. 93–130.Google Scholar
Lill, Kristiansen and Dag, Normann [1997] Total objects in inductively defined types, Archive for Mathematical Logic, vol. 36, no. 6, pp. 405–436.Google Scholar
Jean-Louis, Krivine [1994] Classical logic, storage operators and second-order lambdacalculus, Annals of Pure and Applied Logic, vol. 68, pp. 53–78.Google Scholar
Joseph Bernard, Kruskal [1960] Well-quasi-orderings, the tree theorem and Vaszonyi's conjecture, Transactions of the American Mathematical Society, vol. 95, pp. 210–255.Google Scholar
Kim G., Larsen and Glynn, Winskel [1991] Using information systems to solve recursive domain equations, Information and Computation, vol. 91, pp. 232–258.Google Scholar
Daniel, Leivant [1985] Syntactic translations and provably recursive functions, The Journal of Symbolic Logic, vol. 50, no. 3, pp. 682–688.Google Scholar
Daniel, Leivant [1994] Predicative recurrence in finite type, Logical Foundations of Computer Science (A., Nerode and Y.V., Matiyasevich, editors), Lecture Notes in Computer Science, vol. 813, pp. 227–239.Google Scholar
Daniel, Leivant [1995a] Intrinsic theories and computational complexity, Logic and Computational Complexity, International Workshop LCC'94, Indianapolis, IN, USA, October 1994 (D., Leivant, editor), Lecture Notes in Computer Science, vol. 960, Springer Verlag, Berlin, pp. 177–194.Google Scholar
Daniel, Leivant [1995b] Ramified recurrence and computational complexity I: Word recurrence and poly-time, Feasible Mathematics II (P., Clote and J., Remmel, editors), Birkhäuser, Boston, pp. 320–343.Google Scholar
Daniel, Leivant and Jean-Yves, Marion [1993] Lambda calculus characterization of poly-time, Fundamenta Informaticae, vol. 19, pp. 167–184.Google Scholar
Shih-Ceao, Liu [1960] A theorem on general recursive functions, Proceedings American Mathematical Society, vol. 11, pp. 184–187.Google Scholar
Martin H., Löb [1955] Solution of a problem of Leon Henkin, The Journal of Symbolic Logic, vol. 20, pp. 115–118.Google Scholar
Martin H., Löb and Stanley S., Wainer [1970] Hierarchies of number theoretic functions I, II, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 39–51, 97–113.Google Scholar
Jean-Yves, Marion [2001] Actual arithmetic and feasibility, 15th International workshop, Computer Science Logic, CSL '01 (L., Fribourg, editor), Lecture Notes in Computer Science, vol. 2142, Springer Verlag, Berlin, pp. 115–139.Google Scholar
Per, Martin-Löf [1971] Hauptsatz for the intuitionistic theory of iterated inductive definitions, Proceedings of the Second Scandinavian Logic Symposium (J. E., Fenstad, editor), North-Holland, Amsterdam, pp. 179–216.Google Scholar
Per, Martin-Löf [1972] Infinite terms and a system of natural deduction, Compositio Mathematica, vol. 24, no. 1, pp. 93–103.Google Scholar
Per, Martin-Löf [1983] The domain interpretation of type theory, Talk at the workshop on semantics of programming languages, Chalmers University,Göteborg, August.
Per, Martin-Löf [1984] Intuitionistic Type Theory, Bibliopolis.Google Scholar
John, McCarthy [1963] A basis for a mathematical theory of computation, Computer Programs and Formal Methods, North-Holland, Amsterdam, pp. 33–70.Google Scholar
Grigori, Mints [1973] Quantifier-free and one-quantifier systems, Journal of Soviet Mathematics, vol. 1, pp. 71–84.Google Scholar
Grigori, Mints [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
Grigori, Mints [2000] A Short Introduction to Intuitionistic Logic, Kluwer Academic/Plenum Publishers, New York.Google Scholar
Alexandre, Miquel [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.
F., Lockwood Morris and Cliff B., Jones [1984] An early program proof by Alan Turing, Annals of the History of Computing, vol. 6, pp. 139–143.Google Scholar
Yiannis, Moschovakis [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 (M. L., Dalla Chiara, K., Doets, D., Mundici, and J., van Benthem, editors), Synthese Library, vol. 259, Kluwer Academic Publishers, Dordrecht, Boston, London, pp. 179–208.Google Scholar
Chetan, Murthy [1990] Extracting constructive content from classical proofs, Technical Report 90–1151, Dep. of Comp. Science, Cornell Univ., Ithaca, NewYork, PhD thesis.
John, Myhill [1953] A stumbling block in constructive mathematics (abstract), The Journal of Symbolic Logic, vol. 18, p. 190.Google Scholar
Sara, Negri and Jan von, Plato [2001] Structural Proof Theory, Cambridge University Press.Google Scholar
Maxwell, HermannAlexander, Newman [1942] On theories with a combinatorial definition of “equivalence”, Annals of Mathematics, vol. 43, no. 2, pp. 223–243.Google Scholar
Dag, Normann [2000] Computability over the partial continuous functionals, The Journal of Symbolic Logic, vol. 65, no. 3, pp. 1133–1142.Google Scholar
Dag, Normann [2006] Computing with functionals – computability theory or computer science?, The Bulletin of Symbolic Logic, vol. 12, pp. 43–59.Google Scholar
Piergiorgio, Odifreddi [1999] Classical Recursion Theory Volume II, vol. 143, North-Holland, Amsterdam.Google Scholar
Isabel, Oitavem [2001] Implicit Characterizations of Pspace, Proof Theory in Computer Science (R., Kahle, P., Schroeder-Heister, and R., Stärk, editors), Lecture Bibliography 447 Notes in Computer Science, vol. 2183, Springer Verlag, Berlin, pp. 170–190.Google Scholar
Paulo, Oliva [2006] Unifying functional interpretations, Notre Dame Journal of Formal Logic, vol. 47, pp. 262–290.Google Scholar
Vladimir P., Orevkov [1979] Lower bounds for increasing complexity of derivations after cut elimination, Zapiski Nauchnykh Seminarov Leningradskogo, vol. 88, pp. 137–161.Google Scholar
Geoffrey E., Ostrin and Stanley S., Wainer [2005] Elementary arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 275–292.Google Scholar
Michel, Parigot [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
Jeff, Paris [1980] A hierarchy of cuts in models of arithmetic, Model theory of algebra and arithmetic (L., Pacholski et al., editors), Lecture Notes in Mathematics, vol. 834, Springer Verlag, pp. 312–337.Google Scholar
Jeff, Paris and Leo, Harrington [1977] A mathematical incompleteness in Peano arithmetic, Handbook of Mathematical Logic (J., Barwise, editor), North-Holland, Amsterdam, pp. 1133–1142.Google Scholar
Charles, Parsons [1966] Ordinal recursion in partial systems of number theory (abstract), Notices of the American Mathematical Society, vol. 13, pp. 857–858.Google Scholar
Charles, Parsons [1972] On n-quantifier induction, The Journal of Symbolic Logic, vol. 37, no. 3, pp. 466–482.Google Scholar
Charles, Parsons [1973] Transfinite induction in subsystems of number theory (abstract), The Journal of Symbolic Logic, vol. 38, no. 3, pp. 544–545.Google Scholar
Gordon D., Plotkin [1977] LCF considered as a programming language, Theoretical Computer Science, vol. 5, pp. 223–255.Google Scholar
Gordon D., Plotkin [1978] Tω as a universal domain, Journal of Computer and System Sciences, vol. 17, pp. 209–236.Google Scholar
Wolfram, Pohlers [1998] Subsystems of set theory and second order number theory, Handbook of Proof Theory (S. R., Buss, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam, pp. 209–335.Google Scholar
Wolfram, Pohlers [2009] Proof Theory, Universitext, Springer Verlag, Berlin.Google Scholar
Dag, Prawitz [1965] Natural Deduction, Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy, vol. 3, Almqvist & Wiksell, Stockholm.
Christophe, Raffalli [2004] Getting results from programs extracted from classical proofs, Theoretical Computer Science, vol. 323, pp. 49–70.Google Scholar
Frank Plumpton, Ramsey [1930] On a problem of formal logic, Proceedings of the London Mathematical Society (2), vol. 30, pp. 264–286.Google Scholar
Zygmunt, Ratajczyk [1993] Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic, vol. 64, pp. 95–152.Google Scholar
Paul, Rath [1978] Eine verallgemeinerte Funktionalinterpretation der Heyting Arithmetik endlicher Typen, PhD thesis, Universität Münster, Fachbereich Mathematik.
Michael, Rathjen [1992] A proof-theoretic characterization of primitive recursive set functions, The Journal of Symbolic Logic, vol. 57, pp. 954–969.Google Scholar
Michael, Rathjen [1993] How to develop proof-theoretic ordinal functions on the basis of admissible sets, Mathematical Logic Quarterly, vol. 39, pp. 47–54.Google Scholar
Michael, Rathjen [1999] The realm of ordinal analysis, Sets and Proofs: Logic Colloquium '97 (S. B., Cooper and J. K., Truss, editors), London Mathematical Society Lecture Notes, vol. 258, Cambridge University Press, pp. 219–279.Google Scholar
Michael, Rathjen [2005] Ordinal analysis of parameter free Π12-comprehension, Archive for Mathematical Logic, vol. 44, no. 3, pp. 263–362.Google Scholar
Michael, Rathjen and Andreas, Weiermann [1993] Proof-theoretic investigations on Kruskal's theorem, Annals of Pure and Applied Logic, vol. 60, pp. 49–88.Google Scholar
Diana, Ratiu and Helmut, Schwichtenberg [2010] Decorating proofs, Proofs, Categories and Computations. Essays in honor of Grigori Mints (S., Feferman and W., Sieg, editors), College Publications, pp. 171–188.Google Scholar
Diana, Ratiu and Trifon, Trifonov [2010] Exploring the computational content of the Infinite Pigeonhole Principle, Journal of Logic and Computation, to appear.
Wayne, Richter [1965] Extensions of the constructive ordinals, The Journal of Symbolic Logic, vol. 30, no. 2, pp. 193–211.Google Scholar
Robert, Ritchie [1963] Classes of predictably computable functions, Transactions American Mathematical Society, vol. 106, pp. 139–173.Google Scholar
Joel W., Robbin [1965] Subrecursive Hierarchies, PhD thesis, Princeton University.
Raphael M., Robinson [1950] An essentially undecidable axiom system, Proceedings of the International Congress of Mathematicians (Cambridge 1950), vol. I, pp. 729–730.Google Scholar
Dieter, Rödding [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
Harvey E., Rose [1984] Subrecursion: Functions and Hierarchies, Oxford Logic Guides, vol. 9, Clarendon Press, Oxford.Google Scholar
Barkley, Rosser [1936] Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, vol. 1, pp. 87–91.Google Scholar
Norman A., Routledge [1953] Ordinal recursion, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 49, pp. 175–182.Google Scholar
Jan, Rutten [2000] Universal coalgebra: a theory of systems, Theoretical Computer Science, vol. 249, pp. 3–80.Google Scholar
Diana, Schmidt [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
Peter, Schroeder-Heister [1984] A natural extension of natural deduction, The Journal of Symbolic Logic, vol. 49, pp. 2184–1300.Google Scholar
Kurt, Schütte [1951] Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie, Mathematische Annalen, vol. 122, pp. 369–389.Google Scholar
Kurt, Schütte [1960] Beweistheorie, Springer Verlag, Berlin.Google Scholar
Kurt, Schütte [1977] Proof Theory, Springer Verlag, Berlin.Google Scholar
Helmut, Schwichtenberg [1967] Eine Klassifikation der elementaren Funktionen, Manuscript.Google Scholar
Helmut, Schwichtenberg [1971] Eine Klassifikation der ε0-rekursiven Funktionen, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 17, pp. 61–74.Google Scholar
Helmut, Schwichtenberg [1975] Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion, Logic Colloquium '73 (H. E., Rose and J. C., Shepherdson, editors), North-Holland, Amsterdam, pp. 279–303.Google Scholar
Helmut, Schwichtenberg [1977] Proof theory: some applications of cut-elimination, Handbook of Mathematical Logic (J., Barwise, editor), Studies in Logic and the Foundations of Mathematics, vol. 90, North-Holland, Amsterdam, pp. 867–895.Google Scholar
Helmut, Schwichtenberg [1992] Proofs as programs, Proof Theory (P., Aczel, H., Simmons, and S., Wainer, editors), Cambridge University Press, pp. 81–113.Google Scholar
Helmut, Schwichtenberg [1996] Density and choice for total continuous functionals, Kreiseliana. About and Around Georg Kreisel (P., Odifreddi, editor), A.K. Peters, Wellesley, Massachusetts, pp. 335–362.Google Scholar
Helmut, Schwichtenberg [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
Helmut, Schwichtenberg [2006a] An arithmetic for polynomial-time computation, Theoretical Computer Science, vol. 357, pp. 202–214.Google Scholar
Helmut, Schwichtenberg [2006b] Minlog, The Seventeen Provers of the World (F., Wiedijk, editor), Lecture Notes in Artificial Intelligence, vol. 3600, Springer Verlag, Berlin, pp. 151–157.Google Scholar
Helmut, Schwichtenberg [2006c] Recursion on the partial continuous functionals, Logic Colloquium '05 (C., Dimitracopoulos, L., Newelski, D., Normann, and J., Steel, editors), Lecture Notes in Logic, vol. 28, Association for Symbolic Logic, pp. 173–201.Google Scholar
Helmut, Schwichtenberg [2008a] Dialectica interpretation of well-founded induction, Mathematical Logic Quarterly, vol. 54, no. 3, pp. 229–239.Google Scholar
Helmut, Schwichtenberg [2008b] Realizability interpretation of proofs in constructive analysis, Theory of Computing Systems, vol. 43, no. 3, pp. 583–602.Google Scholar
Helmut, Schwichtenberg and Stephen, Bellantoni [2002] Feasible computation with higher types, Proof and System-Reliability (H., Schwichtenberg and R., Steinbrüggen, editors), Proceedings NATO Advanced Study Institute, Marktoberdorf, 2001, Kluwer Academic Publisher, pp. 399–415.
Helmut, Schwichtenberg and Stanley S., Wainer [1995] Ordinal bounds for programs, Feasible Mathematics II (P., Clote and J., Remmel, editors), Birkhäuser, Boston, pp. 387–406.Google Scholar
Dana, Scott [1970] Outline of a mathematical theory of computation, Technical Monograph PRG-2, Oxford University Computing Laboratory.
Dana, Scott [1982] Domains for denotational semantics, Automata, Languages and Programming (E., Nielsen and E. M., Schmidt, editors), Lecture Notes in Computer Science, vol. 140, Springer Verlag, Berlin, pp. 577–613.Google Scholar
John C., Shepherdson and Howard E., Sturgis [1963] Computability of recursive functions, Journal of the Association for Computing Machinery, vol. 10, pp. 217–255.Google Scholar
Wilfried, Sieg [1985] Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28, pp. 33–71.Google Scholar
Wilfried, Sieg [1991] Herbrand analyses, Archive for Mathematical Logic, vol. 30, pp. 409–441.Google Scholar
Harold, Simmons [1988] The realm of primitive recursion, Archive for Mathematical Logic, vol. 27, pp. 177–188.Google Scholar
Stephen G., Simpson [1985] Nonprovability of certain combinatorial properties of finite trees, Harvey Friedman's Research on the Foundations of Mathematics (L., Harrington, M., Morley, A., Scedrov, and S. G., Simpson, editors), North-Holland, Amsterdam, pp. 87–117.Google Scholar
Stephen G., Simpson [2009] Subsystems of Second Order Arithmetic, second ed., Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press.Google Scholar
Craig, Smoryński [1991] Logical Number Theory I, Universitext, Springer Verlag, Berlin.Google Scholar
Robert I., Soare [1987] Recursively Enumerable Sets and Degrees, Perspectives inMathematical Logic, Springer Verlag, Berlin.Google Scholar
Richard, Sommer [1992] Ordinal arithmetic in IΔ0, Arithmetic, Proof Theory and Computational Complexity (P., Clote and J., Krajicek, editors), Oxford University Press.Google Scholar
Richard, Sommer [1995] Transfinite induction within Peano arithmetic, Annals of Pure and Applied Logic, vol. 76, pp. 231–289.Google Scholar
Elliott J., Spoors [2010] A Hierarchy of Ramified Theories Below Primitive Recursive Arithmetic, PhD thesis, Dept. of Pure Mathematics, Leeds University.
Richard, Statman [1978] Bounds for proof-search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol. 15, pp. 225–287.Google Scholar
Martin, Stein [1976] Interpretationen der Heyting-Arithmetik endlicher Typen, PhD thesis, Universität Münster, Fachbereich Mathematik.
Viggo, Stoltenberg-Hansen, Edward, Griffor, and Ingrid, Lindström [1994] Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
Viggo, Stoltenberg-Hansen and John V., Tucker [1999] Computable rings and fields, Handbook of Computability Theory (Edward, Griffor, editor), North-Holland, Amsterdam, pp. 363–447.Google Scholar
Thomas, Strahm [1997] Polynomial time operations in explicit mathematics, The Journal of Symbolic Logic, vol. 62, no. 2, pp. 575–594.Google Scholar
Thomas, Strahm [2004] A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science, vol. 329, pp. 159–176.Google Scholar
Thomas, Strahm and Jeffery I., Zucker [2008] Primitive recursive selection functions for existential assertions over abstract algebras, Journal of Logic and Algebraic Programming, vol. 76, pp. 175–197.Google Scholar
William W., Tait [1961] Nestedrecursion, Mathematische Annalen, vol. 143, pp. 236–250.Google Scholar
William W., Tait [1968] Normal derivability in classical logic, The Syntax and Semantics of Infinitary Languages (J., Barwise, editor), Lecture Notes in Mathematics, vol. 72, Springer Verlag, Berlin, pp. 204–236.Google Scholar
William W., Tait [1971] Normal form theorem for bar recursive functions of finite type, Proceedings of the Second Scandinavian Logic Symposium (J. E., Fenstad, editor), North-Holland, Amsterdam, pp. 353–367.Google Scholar
Masako, Takahashi [1995] Parallel reductions in λ-calculus, Information and Computation, vol. 118, pp. 120–127.Google Scholar
Gaisi, Takeuti [1967] Consistency proofs of subsystems of classical analysis, Annals of Mathematics, vol. 86, pp. 299–348.Google Scholar
Gaisi, Takeuti [1987] Proof Theory, second ed., North-Holland, Amsterdam.Google Scholar
Alfred, Tarski [1936] Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, vol. 1, pp. 261–405.Google Scholar
Trifon, Trifonov [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
Anne S., Troelstra [1973] Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer Verlag, Berlin.Google Scholar
Anne S., Troelstra and Helmut, Schwichtenberg [2000] Basic Proof Theory, second ed., Cambridge University Press.Google Scholar
Anne S., Troelstra and Dirk van, Dalen [1988] Constructivism in Mathematics. An Introduction, Studies in Logic and the Foundations of Mathematics, vol. 121, 123, North-Holland, Amsterdam.Google Scholar
John V., Tucker and Jeffery I., Zucker [1992] Provable computable selection functions on abstract structures, Proof Theory (P., Aczel, H., Simmons, and S., Wainer, editors), Cambridge University Press, pp. 275–306.Google Scholar
John V., Tucker and Jeffery I., Zucker [2000] Computable functions and semicomputable sets on many-sorted algebras, Handbook of Logic in Computer Science, Vol. V (S., Abramsky, D., Gabbay, and T., Maibaum, editors), Oxford University Press, pp. 317–523.Google Scholar
John V., Tucker and Jeffery I., Zucker [2006] Abstract versus concrete computability: the case of countable algebras, Logic Colloquium 2003 (V., Stoltenberg-Hansen and J., Väänänen, editors), ASL Lecture Notes in Logic, vol. 24, AK Peters, pp. 377–408.Google Scholar
Jaco van de, Pol [1995] Two different strong normalization proofs?, HOA 1995 (G., Dowek, J., Heering, K., Meinke, and B., Möller, editors), Lecture Notes in Computer Science, vol. 1074, Springer Verlag, Berlin, pp. 201–220.Google Scholar
Femke van, Raamsdonk and Paula, Severi [1995] On normalisation, Computer Science Report CS-R9545 1995, Centrum voor Wiskunde en Informatica.
Jan von, Plato [2008] Gentzen's proof of normalization for natural deduction, The Bulletin of Symbolic Logic, vol. 14, no. 2, pp. 240–257.Google Scholar
Stanley S., Wainer [1970] A classification of the ordinal recursive functions, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 136–153.Google Scholar
Stanley S., Wainer [1972] Ordinal recursion, and a refinement of the extended Grzegorcyk hierarchy, The Journal of Symbolic Logic, vol. 38, pp. 281–292.Google Scholar
Stanley S., Wainer [1989] Slow growing versus fast growing, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 608–614.Google Scholar
Stanley S., Wainer [1999] Accessible recursive functions, The Bulletin of Symbolic Logic, vol. 5, no. 3, pp. 367–388.Google Scholar
Stanley S., Wainer [2010] Computing bounds from arithmetical proofs, Ways of Proof Theory: Festschrift for W. Pohlers (R., Schindler, editor), Ontos Verlag, pp. 459–476.Google Scholar
Stanley S., Wainer and Richard S., Williams [2005] Inductive definitions over a predicative arithmetic, Annals of Pure and Applied Logic, vol. 136, pp. 175–188.Google Scholar
Andreas, Weiermann [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
Stanley S., Wainer [1996] How to characterize provably total functions by local predicativity, The Journal of Symbolic Logic, vol. 61, no. 1, pp. 52–69.Google Scholar
Stanley S., Wainer [1999] What makes a (pointwise) subrecursive hierarchy slow growing?, Sets and Proofs: Logic Colloquium '97 (S. B., Cooper and J. K., Truss, editors), London Mathematical Society Lecture Notes, vol. 258, Cambridge University Press, pp. 403–423.Google Scholar
Stanley S., Wainer [2004] A classification of rapidly growing Ramsey functions, Proceedings of the American Mathematical Society, vol. 132, pp. 553–561.Google Scholar
Stanley S., Wainer [2005] Analytic combinatorics, proof-theoretic ordinals, and phasetransitions for independence results, Annals of Pure and Applied Logic, vol. 136, pp. 189–218.Google Scholar
Stanley S., Wainer [2006] Classifying the provably total functions of PA, The Bulletin of Symbolic Logic, vol. 12, pp. 177–190.Google Scholar
Stanley S., Wainer [2007] Phase transition thresholds for some Friedman-style independence results, Mathematical Logic Quarterly, vol. 53, pp. 4–18.Google Scholar
Richard S., Williams [2004] Finitely Iterated Inductive Definitions over a Predicative Arithmetic, PhD thesis, Department of Pure Mathematics, Leeds University.
Fred, Zemke [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
Jeffrey, Zucker [1973] Iterated inductivex1 definitions, trees and ordinals, Mathematical Investigation of Intuitionistic Arithmetic and Analysis (A. S., Troelstra, editor), Lecture Notes in Mathematics, vol. 344, Springer Verlag, Berlin, pp. 392–453.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×