ReferencesAndreas, 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.
Samson, Abramsky [1991] Domain theory in logical form, Annals of Pure and Applied Logic, vol. 51, pp. 1–77.
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.
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.
Roberto M., Amadio and Pierre-Louis, Curien [1998] Domains and Lambda-Calculi, Cambridge University Press.
Toshiyasu, Arai [1991] A slow growing analogue to Buchholz' proof, Annals of Pure and Applied Logic, vol. 54, pp. 101–120.
Toshiyasu, Arai [2000] Ordinal diagrams for recursively Mahlo universes, Archive for Mathematical Logic, vol. 39, no. 5, pp. 353–391.
Jeremy, Avigad [2000] Interpreting classical theories in constructive ones, The Journal of Symbolic Logic, vol. 65, no. 4, pp. 1785–1812.
Jeremy, Avigad and Rick, Sommer [1997] A model theoretic approach to ordinal analysis, The Bulletin of Symbolic Logic, vol. 3, pp. 17–52.
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.
Hendrik, Pieter Barendregt [1984] The Lambda Calculus, second ed., North-Holland, Amsterdam.
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.
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.
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.
Lev D., Beklemishev [2003] Proof-theoretic analysis of iterated reflection, Archive for Mathematical Logic, vol. 42, no. 6, pp. 515–552.
Stephen, Bellantoni and Stephen, Cook [1992] A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol. 2, pp. 97–110.
Stephen, Bellantoni and Martin, Hofmann [2002] A new “feasible” arithmetic, The Journal of Symbolic Logic, vol. 67, no. 1, pp. 104–116.
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.
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.
Ulrich, Berger [1993b] Total sets and objects in domain theory, Annals of Pure and Applied Logic, vol. 60, pp. 91–117.
Ulrich, Berger [2005a] Continuous semantics for strong normalization, Proceedings CiE 2005, Lecture Notes in Computer Science, vol. 3526, pp. 23–34.
Ulrich, Berger [2005b] Uniform Heyting arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 125–148.
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.
Ulrich, Berger, Stefan, Berghofer, Pierre, Letouzey, and Helmut, Schwichtenberg [2006] Program extraction from normalization proofs, Studia Logica, vol. 82, pp. 27–51.
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.
Ulrich, Berger, Matthias, Eberl, and Helmut, Schwichtenberg [2003] Term rewriting for normalization by evaluation, Information and Computation, vol. 183, pp. 19–42.
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.
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.
Evert, Willem Beth [1956] Semantic construction of intuitionistic logic, Medelingen de KNAW N.S., vol. 19, no. 11.
Evert, Willem Beth [1959] The Foundations of Mathematics, North-Holland, Amsterdam.
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.
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.
Egon, Börger, Erich, Grädel, and Yuri, Gurevich [1997] The Classical Decision Problem, Perspectives in Mathematical Logic, Springer Verlag, Berlin.
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.
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.
Wilfried, Buchholz, Adam, Cichon, and Andreas, Weiermann [1994] A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 40, pp. 273–286.
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.
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.
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.
Samuel R., Buss [1986] Bounded Arithmetic, Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli.
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.
Samuel R., Buss [1998a] First order proof theory of arithmetic, Handbook of Proof Theory (S., Buss, editor), North-Holland, Amsterdam, pp. 79–147.
Samuel R., Buss [1998b] Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam.
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.
Andrea, Cantini [2002] Polytime, combinatory logic and positive safe induction, Archive for Mathematical Logic, vol. 41, no. 2, pp. 169–189.
Timothy J., Carlson [2001] Elementary patterns of resemblance, Annals of Pure and Applied Logic, vol. 108, pp. 19–77.
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).
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.
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.
John P., Cleave [1963] A hierarchy of primitive recursive functions, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 9, pp. 331–345.
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.
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.
Robert L., Constable [1972] Subrecursive programming languages I: efficiency and program structure, Journal of the ACM, vol. 19, pp. 526–568.
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.
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.
S. Barry, Cooper [2003] Computability Theory, Shapman Hall/CRC.
,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.
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.
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.
Thierry, Coquand and Arnaud, Spiwack [2006] A proof of strong normalisation using domain theory, Proceedings LICS 2006, pp. 307–316.
Haskell B., Curry [1930] Grundlagen der kombinatorischen Logik, American Journal of Mathematics, vol. 52, pp. 509–536, 789–834.
Nigel J., Cutland [1980] Computability: An Introduction to Recursive Function Theory, Cambridge University Press.
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.
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.
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.
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.
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.
Yuri L., Ershov [1977] ModelC of partial continuous functionals, Logic colloquium 1976 (R., Gandy and M., Hyland, editors), North-Holland, Amsterdam, pp. 455–467.
Matthew V. H., Fairtlough and Stanley S., Wainer [1992] Ordinal complexity of recursive definitions, Information and Computation, vol. 99, pp. 123–153.
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.
Solomon, Feferman [1960] Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae, vol. XLIX, pp. 35–92.
Solomon, Feferman [1962] Classifications of recursive functions by means of hierarchies, Transactions American Mathematical Society, vol. 104, pp. 101–122.
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.
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.
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.
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.
Solomon, Feferman and Thomas, Strahm [2000] The unfolding of non-finitist arithmetic, Annals of Pure and Applied Logic, vol. 104, pp. 75–96.
Solomon, Feferman and Thomas, Strahm [2010] Unfolding finitist arithmetic, Review of Symbolic Logic, vol. 3, pp. 665–689.
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.
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.
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.
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.
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.
Harvey, Friedman [1981] Independence results in finite graph theory, Unpublished manuscripts, Ohio State University, 76 pages.
Harvey, Friedman [1982] Beyond Kruskal's theorem I–III, Unpublished manuscripts, Ohio State University, 48 pages.
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.
Harvey, Friedman and Michael, Sheard [1995] Elementary descent recursion and proof theory, Annals of Pure and Applied Logic, vol. 71, pp. 1–45.
Gerhard, Gentzen [1935] Untersuchungen über das logische Schließen I, II, Mathematische Zeitschrift, vol. 39, pp. 176–210, 405–431.
Gerhard, Gentzen [1936] Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112, pp. 493–565.
Gerhard, Gentzen [1943] Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie, Mathematische Annalen, vol. 119, pp. 140–161.
Philipp, Gerhardy and Ulrich, Kohlenbach [2008] General logical metatheorems for functional analysis, Transactions of the American Mathematical Society, vol. 360, pp. 2615–2660.
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.
Jean-Yves, Girard [1981] Π12-logic. Part I: Dilators, Annals of Mathematical Logic, vol. 21, pp. 75–219.
Jean-Yves, Girard [1987] Proof Theory and Logical Complexity, Bibliopolis, Napoli.
Jean-Yves, Girard [1998] Light linear logic, Information and Computation, vol. 143, pp. 175–204.
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.
Kurt, Gödel [1958] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts, Dialectica, vol. 12, pp. 280–287.
Ruben L., Goodstein [1944] On the restricted ordinal theorem, The Journal of Symbolic Logic, vol. 9, pp. 33–41.
Ronald, Graham, Bruce, Rothschild, and Joel, Spencer [1990] Ramsey Theory, second ed., Discrete Mathematics and Optimization, Wiley Interscience.
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.
Andrzey, Grzegorczyk [1953] Some Classes of Recursive Functions, Rozprawy Matematyczne, Warszawa.
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.
Petr, Hájek and Pavel, Pudlák [1993] Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer Verlag, Berlin.
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.
Godfrey H., Hardy [1904] A theorem concerning the infinite cardinal numbers, Quaterly Journal of Mathematics, vol. 35, pp. 87–94.
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.
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.
Arend, Heyting [1959] Constructivity in mathematics, North-Holland, Amsterdam.
David, Hilbert and Paul, Bernays [1939] Grundlagen der Mathematik, vol. II, Springer Verlag, Berlin.
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.
Martin, Hofmann [2000] Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol. 104, pp. 113–166.
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.
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.
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.
Gerhard, Jäger [1986] Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibliopolis, Naples.
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.
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.
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.
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.
Carl G., Jockusch [1972] Ramsey's theorem and recursion theory, The Journal of Symbolic Logic, vol. 37, pp. 268–280.
Ingebrigt, Johansson [1937] Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, vol. 4, pp. 119–136.
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.
Lazlo, Kalmár [1943] Ein einfaches Beispiel für ein unentscheidbares Problem (Hungarian, with German summary), Mat. Fiz. Lapok, vol. 50, pp. 1–23.
Jussi, Ketonen and Robert M., Solovay [1981] Rapidly growing Ramsey furnctions, Annals of Mathematics (2), vol. 113, pp. 267–314.
Akiko, Kino, John, Myhill, and Richard E., Vesley [1970] Intuitioninism and Proof Theory, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.
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.
Stephen C., Kleene [1952] Introduction to Metamathematics, D., van Nostrand, New York.
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.
Ulrich, Kohlenbach [2005] Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357, pp. 89–128.
Ulrich, Kohlenbach [2008] Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Verlag, Berlin.
Ulrich, Kohlenbach and Laurentin, Leustean [2003] Mann iterates of directionally nonexpansive mappings in hyperbolic spaces, Abstracts in Applied Analysis, vol. 8, pp. 449–477.
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.
Ulrich, Kohlenbach and Paulo, Oliva [2003b] Proof mining in L1 approximation, Annals of Pure and Applied Logic, vol. 121, pp. 1–38.
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.
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.
Georg, Kreisel [1952] On the interpretation of non-finitist proofs II, The Journal of Symbolic Logic, vol. 17, pp. 43–58.
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.
Georg, Kreisel [1963] Generalized inductive definitions, Reports for the seminar on foundations of analysis, vol. I, Stanford University, mimeographed.
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.
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.
Lill, Kristiansen and Dag, Normann [1997] Total objects in inductively defined types, Archive for Mathematical Logic, vol. 36, no. 6, pp. 405–436.
Jean-Louis, Krivine [1994] Classical logic, storage operators and second-order lambdacalculus, Annals of Pure and Applied Logic, vol. 68, pp. 53–78.
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.
Kim G., Larsen and Glynn, Winskel [1991] Using information systems to solve recursive domain equations, Information and Computation, vol. 91, pp. 232–258.
Daniel, Leivant [1985] Syntactic translations and provably recursive functions, The Journal of Symbolic Logic, vol. 50, no. 3, pp. 682–688.
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.
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.
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.
Daniel, Leivant and Jean-Yves, Marion [1993] Lambda calculus characterization of poly-time, Fundamenta Informaticae, vol. 19, pp. 167–184.
Shih-Ceao, Liu [1960] A theorem on general recursive functions, Proceedings American Mathematical Society, vol. 11, pp. 184–187.
Martin H., Löb [1955] Solution of a problem of Leon Henkin, The Journal of Symbolic Logic, vol. 20, pp. 115–118.
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.
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.
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.
Per, Martin-Löf [1972] Infinite terms and a system of natural deduction, Compositio Mathematica, vol. 24, no. 1, pp. 93–103.
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.
John, McCarthy [1963] A basis for a mathematical theory of computation, Computer Programs and Formal Methods, North-Holland, Amsterdam, pp. 33–70.
Grigori, Mints [1973] Quantifier-free and one-quantifier systems, Journal of Soviet Mathematics, vol. 1, pp. 71–84.
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).
Grigori, Mints [2000] A Short Introduction to Intuitionistic Logic, Kluwer Academic/Plenum Publishers, New York.
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.
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.
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.
Sara, Negri and Jan von, Plato [2001] Structural Proof Theory, Cambridge University Press.
Maxwell, HermannAlexander, Newman [1942] On theories with a combinatorial definition of “equivalence”, Annals of Mathematics, vol. 43, no. 2, pp. 223–243.
Dag, Normann [2000] Computability over the partial continuous functionals, The Journal of Symbolic Logic, vol. 65, no. 3, pp. 1133–1142.
Dag, Normann [2006] Computing with functionals – computability theory or computer science?, The Bulletin of Symbolic Logic, vol. 12, pp. 43–59.
Piergiorgio, Odifreddi [1999] Classical Recursion Theory Volume II, vol. 143, North-Holland, Amsterdam.
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.
Paulo, Oliva [2006] Unifying functional interpretations, Notre Dame Journal of Formal Logic, vol. 47, pp. 262–290.
Vladimir P., Orevkov [1979] Lower bounds for increasing complexity of derivations after cut elimination, Zapiski Nauchnykh Seminarov Leningradskogo, vol. 88, pp. 137–161.
Geoffrey E., Ostrin and Stanley S., Wainer [2005] Elementary arithmetic, Annals of Pure and Applied Logic, vol. 133, pp. 275–292.
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.
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.
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.
Charles, Parsons [1966] Ordinal recursion in partial systems of number theory (abstract), Notices of the American Mathematical Society, vol. 13, pp. 857–858.
Charles, Parsons [1972] On n-quantifier induction, The Journal of Symbolic Logic, vol. 37, no. 3, pp. 466–482.
Charles, Parsons [1973] Transfinite induction in subsystems of number theory (abstract), The Journal of Symbolic Logic, vol. 38, no. 3, pp. 544–545.
Gordon D., Plotkin [1977] LCF considered as a programming language, Theoretical Computer Science, vol. 5, pp. 223–255.
Gordon D., Plotkin [1978] Tω as a universal domain, Journal of Computer and System Sciences, vol. 17, pp. 209–236.
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.
Wolfram, Pohlers [2009] Proof Theory, Universitext, Springer Verlag, Berlin.
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.
Frank Plumpton, Ramsey [1930] On a problem of formal logic, Proceedings of the London Mathematical Society (2), vol. 30, pp. 264–286.
Zygmunt, Ratajczyk [1993] Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic, vol. 64, pp. 95–152.
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.
Michael, Rathjen [1993] How to develop proof-theoretic ordinal functions on the basis of admissible sets, Mathematical Logic Quarterly, vol. 39, pp. 47–54.
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.
Michael, Rathjen [2005] Ordinal analysis of parameter free Π12-comprehension, Archive for Mathematical Logic, vol. 44, no. 3, pp. 263–362.
Michael, Rathjen and Andreas, Weiermann [1993] Proof-theoretic investigations on Kruskal's theorem, Annals of Pure and Applied Logic, vol. 60, pp. 49–88.
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.
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.
Robert, Ritchie [1963] Classes of predictably computable functions, Transactions American Mathematical Society, vol. 106, pp. 139–173.
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.
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.
Harvey E., Rose [1984] Subrecursion: Functions and Hierarchies, Oxford Logic Guides, vol. 9, Clarendon Press, Oxford.
Barkley, Rosser [1936] Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, vol. 1, pp. 87–91.
Norman A., Routledge [1953] Ordinal recursion, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 49, pp. 175–182.
Jan, Rutten [2000] Universal coalgebra: a theory of systems, Theoretical Computer Science, vol. 249, pp. 3–80.
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.
Peter, Schroeder-Heister [1984] A natural extension of natural deduction, The Journal of Symbolic Logic, vol. 49, pp. 2184–1300.
Kurt, Schütte [1951] Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie, Mathematische Annalen, vol. 122, pp. 369–389.
Kurt, Schütte [1960] Beweistheorie, Springer Verlag, Berlin.
Kurt, Schütte [1977] Proof Theory, Springer Verlag, Berlin.
Helmut, Schwichtenberg [1967] Eine Klassifikation der elementaren Funktionen, Manuscript.
Helmut, Schwichtenberg [1971] Eine Klassifikation der ε0-rekursiven Funktionen, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 17, pp. 61–74.
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.
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.
Helmut, Schwichtenberg [1992] Proofs as programs, Proof Theory (P., Aczel, H., Simmons, and S., Wainer, editors), Cambridge University Press, pp. 81–113.
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.
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.
Helmut, Schwichtenberg [2006a] An arithmetic for polynomial-time computation, Theoretical Computer Science, vol. 357, pp. 202–214.
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.
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.
Helmut, Schwichtenberg [2008a] Dialectica interpretation of well-founded induction, Mathematical Logic Quarterly, vol. 54, no. 3, pp. 229–239.
Helmut, Schwichtenberg [2008b] Realizability interpretation of proofs in constructive analysis, Theory of Computing Systems, vol. 43, no. 3, pp. 583–602.
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.
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.
John C., Shepherdson and Howard E., Sturgis [1963] Computability of recursive functions, Journal of the Association for Computing Machinery, vol. 10, pp. 217–255.
Wilfried, Sieg [1985] Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28, pp. 33–71.
Wilfried, Sieg [1991] Herbrand analyses, Archive for Mathematical Logic, vol. 30, pp. 409–441.
Harold, Simmons [1988] The realm of primitive recursion, Archive for Mathematical Logic, vol. 27, pp. 177–188.
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.
Stephen G., Simpson [2009] Subsystems of Second Order Arithmetic, second ed., Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press.
Craig, Smoryński [1991] Logical Number Theory I, Universitext, Springer Verlag, Berlin.
Robert I., Soare [1987] Recursively Enumerable Sets and Degrees, Perspectives inMathematical Logic, Springer Verlag, Berlin.
Richard, Sommer [1992] Ordinal arithmetic in IΔ0, Arithmetic, Proof Theory and Computational Complexity (P., Clote and J., Krajicek, editors), Oxford University Press.
Richard, Sommer [1995] Transfinite induction within Peano arithmetic, Annals of Pure and Applied Logic, vol. 76, pp. 231–289.
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.
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.
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.
Thomas, Strahm [1997] Polynomial time operations in explicit mathematics, The Journal of Symbolic Logic, vol. 62, no. 2, pp. 575–594.
Thomas, Strahm [2004] A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science, vol. 329, pp. 159–176.
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.
William W., Tait [1961] Nestedrecursion, Mathematische Annalen, vol. 143, pp. 236–250.
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.
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.
Masako, Takahashi [1995] Parallel reductions in λ-calculus, Information and Computation, vol. 118, pp. 120–127.
Gaisi, Takeuti [1967] Consistency proofs of subsystems of classical analysis, Annals of Mathematics, vol. 86, pp. 299–348.
Gaisi, Takeuti [1987] Proof Theory, second ed., North-Holland, Amsterdam.
Alfred, Tarski [1936] Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, vol. 1, pp. 261–405.
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.
Anne S., Troelstra [1973] Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer Verlag, Berlin.
Anne S., Troelstra and Helmut, Schwichtenberg [2000] Basic Proof Theory, second ed., Cambridge University Press.
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.
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.
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.
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.
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.
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.
Stanley S., Wainer [1970] A classification of the ordinal recursive functions, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 136–153.
Stanley S., Wainer [1972] Ordinal recursion, and a refinement of the extended Grzegorcyk hierarchy, The Journal of Symbolic Logic, vol. 38, pp. 281–292.
Stanley S., Wainer [1989] Slow growing versus fast growing, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 608–614.
Stanley S., Wainer [1999] Accessible recursive functions, The Bulletin of Symbolic Logic, vol. 5, no. 3, pp. 367–388.
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.
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.
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.
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.
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.
Stanley S., Wainer [2004] A classification of rapidly growing Ramsey functions, Proceedings of the American Mathematical Society, vol. 132, pp. 553–561.
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.
Stanley S., Wainer [2006] Classifying the provably total functions of PA, The Bulletin of Symbolic Logic, vol. 12, pp. 177–190.
Stanley S., Wainer [2007] Phase transition thresholds for some Friedman-style independence results, Mathematical Logic Quarterly, vol. 53, pp. 4–18.
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.
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.
