Posted by N. Pischke - 11.02.25
The list given here is an attempt to collect some of the many relevant references for works from and around the area of proof mining. For simplicity, the focus is (initially) on applications in analysis and on applications using functional interpretations. Through the breadth of this goal, the list nevertheless will presumably always be incomplete.
Suggestions for additions can be send to pischke@mathematik.tu-darmstadt.de.
The references are ordered in reverse chronological order by year. Click here for a PDF version.
| [1] | M. Neri, N. Pischke, and T. Powell. Generalized learnability of stochastic principles. 2025. Manuscript available at https://nicholaspischke.github.io/. |
| [2] | M. Neri. Quantitative Strong Laws of Large Numbers. Electronic Journal of Probability, 30, 2025. 20, 22pp., DOI. |
| [3] | U. Kohlenbach and N. Pischke. Quantitative results for a Tseng-type primal-dual method for composite monotone inclusions. 2024. Manuscript available at https://nicholaspischke.github.io/. |
| [4] | N. Pischke. A proof-theoretic bound extraction theorem for monotone operators in Banach spaces. 2024. Manuscript available at https://nicholaspischke.github.io/. |
| [5] | N. Pischke. On logical aspects of extensionality and continuity for set-valued operators with applications to nonlinear analysis. 2024. Manuscript available at https://nicholaspischke.github.io/. |
| [6] | P. Pinto and N. Pischke. On the Halpern method with adaptive anchoring parameters. 2024. DOI. |
| [7] | N. Pischke and T. Powell. Asymptotic regularity of a generalised stochastic Halpern scheme with applications. arXiv preprint, arXiv:2411.04845, 2024. |
| [8] | N. Pischke. On the proximal point algorithm for strongly quasiconvex functions in Hadamard spaces. arXiv preprint, arXiv:2411.06910, 2024. |
| [9] | P. Pinto and A. Sipoş. Products of hyperbolic spaces. arXiv preprint, arXiv:2408.14093, 2024. |
| [10] | M. Neri and T. Powell. A quantitative Robbins-Siegmund theorem. arXiv preprint, arXiv:2410.15986, 2024. |
| [11] | M. Neri. A finitary Kronecker's lemma and large deviations in the Strong Law of Large numbers on Banach spaces. arXiv preprint, arXiv:2411.08620, 2024. |
| [12] | J. Treusch and U. Kohlenbach. Rates of convergence for splitting algorithms. Israel Journal of Mathematics, 2024. To appear. |
| [13] | L.M. Després and U. Kohlenbach. Herbrand analyses in geometry: a case study. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~kohlenbach/. |
| [14] | L. Sauras-Altuzarra. Some applications of Baaz's generalization method to the study of the factors of Fermat numbers. Journal of Logic and Computation, 34(6):1199--1209, 2024. DOI. |
| [15] | H. Towsner. What do ultraproducts remember about the original structures? Journal of Logic and Computation, 34(1):125--160, 2024. DOI. |
| [16] | P. Pinto and N. Pischke. On Dykstra's algorithm with Bregman projections. Oberwolfach Preprint 2024-04, 2024. DOI. |
| [17] | M. Neri and N. Pischke. Proof mining and probability theory. arXiv preprint, arXiv:2403.00659, 2024. |
| [18] | P. Firmino and P. Pinto. The alternating Halpern-Mann iteration for families of maps. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~pinto/. |
| [19] | P. Pinto. Proof mining and the convex feasibility problem: the curious case of Dykstra's algorithm. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~pinto/. |
| [20] | P. Firmino and L. Leuştean. Quantitative asymptotic regularity of the VAM iteration with error terms for m-accretive operators in Banach spaces. Zeitschrift für Analysis und ihre Anwendungen, 2024. To appear. DOI. |
| [21] | M. Neri and T. Powell. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales. arXiv preprint, arXiv:2406.19979, 2024. |
| [22] | N. Pischke. Logical Metatheorems for Accretive and (Generalized) Monotone Set-Valued Operators. Journal of Mathematical Logic, 24(2), 2024. 2350008, 59pp., DOI. |
| [23] | B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. Fixed Point Theory, 25(1):61--98, 2024. DOI. |
| [24] | L. Leuştean and P. Pinto. Rates of asymptotic regularity for the alternating Halpern-Mann iteration. Optimization Letters, 18:529--543, 2024. DOI. |
| [25] | H. Cheval and L. Leuştean. Linear rates of asymptotic regularity for Halpern-type iterations. Mathematics of Computation, 2024. To appear. DOI. |
| [26] | A. Sipoş. On quantitative metastability for accretive operators. Zeitschrift für Analysis und ihre Anwendungen, 43(3/4):417--433, 2024. DOI. |
| [27] | P. Pinto. On the finitary content of Dykstra's cyclic projections algorithm. Zeitschrift für Analysis und ihre Anwendungen, 2024. To appear. DOI. |
| [28] | U. Kohlenbach and P. Pinto. Fejér monotone sequences revisited. Journal of Convex Analysis, 2024. To appear. |
| [29] | R. Findling and U. Kohlenbach. Rates of convergence and metastability for Chidume's algorithm for the approximation of zeros of accretive operators in Banach spaces. Numerical Functional Analysis and Optimization, 45(3):216--233, 2024. DOI. |
| [30] | N. Pischke. Rates of convergence for the asymptotic behavior of second-order Cauchy problems. Journal of Mathematical Analysis and Applications, 533(2), 2024. 128078, 15pp., DOI. |
| [31] | N. Pischke. Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions. Transactions of the American Mathematical Society, 377(10):7475--7517, 2024. DOI. |
| [32] | N. Pischke. Generalized Fejér monotone sequences and their finitary content. Optimization, 2024. To appear. DOI. |
| [33] | N. Pischke and U. Kohlenbach. Effective rates for iterations involving Bregman strongly nonexpansive operators. Set-Valued and Variational Analysis, 32(4), 2024. 33, 58pp., DOI. |
| [34] | N. Pischke. Duality, Fréchet differentiability and Bregman distances in hyperbolic spaces. Israel Journal of Mathematics, 2024. To appear. |
| [35] | P. Pinto. Nonexpansive maps in nonlinear smooth spaces. Transactions of the American Mathematical Society, 377(9):6379--6426, 2024. DOI. |
| [36] | T. Powell. Proof mining and informal proof theoretic reasoning: A case study on greedy approximation schemes. 2024. Manuscript available at https://t-powell.github.io/publications.html. |
| [37] | H. Cheval. Rates of asymptotic regularity of the Tikhonov-Mann iteration for families of mappings. Revue Roumaine de Mathématiques Pures et Appliquées, 2023. To appear. |
| [38] | U. Kohlenbach. Kreisel's `shift of emphasis' and contemporary proof mining. Studies in Logic, 16(3):1--35, 2023. |
| [39] | H. Towsner. From Saturated Embedding Tests to Explicit Algorithms. arXiv preprint, arXiv:2306.12239, 2023. |
| [40] | T. Powell. A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory. Annals of Pure and Applied Logic, 174(4):103231, 2023. DOI. |
| [41] | M. Neri and T. Powell. A computational study of a class of recursive inequalities. Journal of Logic and Analysis, 15(3):1--48, 2023. DOI. |
| [42] | N. Pischke. Quantitative Results on Algorithms for Zeros of Differences of Monotone Operators in Hilbert Space. Journal of Convex Analysis, 30(1):295--315, 2023. |
| [43] | N. Pischke. On Korpelevich's Extragradient Algorithm. Zeitschrift für Analysis und ihre Anwendungen, 42(1/2):117--129, 2023. DOI. |
| [44] | L. Pǎunescu and A. Sipoş. A proof-theoretic metatheorem for tracial von Neumann algebras. Mathematical Logic Quarterly, 69(1):63--76, 2023. DOI. |
| [45] | B. Dinis and P. Pinto. Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces. SIAM Journal on Optimization, 33(2):785--815, 2023. DOI. |
| [46] | H. Cheval, U. Kohlenbach, and L. Leustean. On modified Halpern and Tikhonov-Mann iterations. Journal of Optimization Theory and Applications, 197:233--251, 2023. DOI. |
| [47] | U. Kohlenbach and N. Pischke. Proof theory and nonsmooth analysis. Philosophical Transactions of the Royal Society A, 381(2248):21pp., 2023. DOI. |
| [48] | A. Freund and U. Kohlenbach. Bounds for a nonlinear ergodic theorem for Banach spaces. Ergodic Theory and Dynamical Systems, 43:1570--1593, 2023. DOI. |
| [49] | A. Sipoş. The computational content of super strongly nonexpansive mappings and uniformly monotone operators. Israel Journal of Mathematics, 2023. To appear. |
| [50] | P. Pinto and N. Pischke. On computational properties of Cauchy problems generated by accretive operators. Documenta Mathematica, 28(5):1235--1274, 2023. DOI. |
| [51] | N. Pischke. A Proof-Theoretic Metatheorem for Nonlinear Semigroups generated by an Accretive Operator and Applications. arXiv preprint, arXiv:2304.01723, 2023. |
| [52] | H. Cheval and L. Leuştean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration. Optimization Methods and Software, 37:2225--2240, 2022. DOI. |
| [53] | A. Sipoş. Abstract strongly convergent variants of the proximal point algorithm. Computational Optimization and Applications, 83(1):349--380, 2022. DOI. |
| [54] | A. Sipoş. Revisiting jointly firmly nonexpansive families of mappings. Optimization, 71(13):3819--3834, 2022. DOI. |
| [55] | A. Sipoş. On extracting variable Herbrand disjunctions. Studia Logica, 110(4):1115--1134, 2022. DOI. |
| [56] | A. Sipoş. Quantitative inconsistent feasibility for averaged mappings. Optimization Letters, 16(6):1915--1925, 2022. DOI. |
| [57] | A. Freund and U. Kohlenbach. R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces. Applied Set-Valued Analysis and Optimization, 4:323--336, 2022. DOI. |
| [58] | U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. Journal of Mathematical Analysis and Applications, 507:125823, 33pp., 2022. DOI. |
| [59] | U. Kohlenbach. On the Proximal Point Algorithm and its Halpern-type variant for generalized monotone operators in Hilbert space. Optimization Letters, 16:611--621, 2022. DOI. |
| [60] | N. Pischke and U. Kohlenbach. Quantitative analysis of a subgradient-type method for equilibrium problems. Numerical Algorithms, 90:197--219, 2022. DOI. |
| [61] | A. Koutsoukou-Argyraki. On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy. In Connecting with Computability. CiE 2021, volume 12813 of LNCS, pages 285--296. Springer, 2021. DOI. |
| [62] | F. Ferreira. The abstract type of the real number. Archive for Mathematical Logic, 60(7--8):1005--1017, 2021. DOI. |
| [63] | R. Arthan and P. Oliva. On the Borel-Cantelli Lemmas, the Erdós-Rényi Theorem, and the Kochen-Stone Theorem. Journal of Logic and Analysis, 13(6):1--23, 2021. DOI. |
| [64] | T. Powell and F. Wiesnet. Rates of convergence for asymptotically weakly contractive mappings in normed spaces. Numerical Functional Analysis and Optimization, 42(15):1802--1838, 2021. DOI. |
| [65] | A. Sipoş. Bounds on strong unicity for Chebyshev approximation with bounded coefficients. Mathematische Nachrichten, 294(12):2425--2440, 2021. DOI. |
| [66] | A. Sipoş. A quantitative multiparameter mean ergodic theorem. Pacific Journal of Mathematics, 314(1):209--218, 2021. DOI. |
| [67] | A. Sipoş. Construction of fixed points of asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces. Numerical Functional Analysis and Optimization, 42(6):696--711, 2021. DOI. |
| [68] | A. Sipoş. Rates of metastability for iterations on the unit interval. Journal of Mathematical Analysis and Applications, 502(1):125235, 11pp., 2021. DOI. |
| [69] | P. Pinto. A Rate of Metastability for the Halpern Type Proximal Point Algorithm. Numerical Functional Analysis and Optimization, 42(3):320--343, 2021. DOI. |
| [70] | B. Dinis and P. Pinto. Quantitative Results on the Multi-Parameters Proximal Point Algorithm. Journal of Convex Analysis, 28(3):729--750, 2021. |
| [71] | L. Leuştean and P. Pinto. Quantitative results on a Halpern-type proximal point algorithm. Computational Optimization and Applications, 79(1):101--125, 2021. DOI. |
| [72] | B. Dinis and P. Pinto. On the convergence of algorithms with Tikhonov regularization terms. Optimization Letters, 15(4):1263--1276, 2021. DOI. |
| [73] | U. Kohlenbach. Proof-theoretic uniform boundedness and bounded collection principles and Heine-Borel compactness. Archive for Mathematical Logic, 60:995--1003, 2021. DOI. |
| [74] | U. Kohlenbach, G. Lopez-Acedo, and A. Nicolae. A uniform betweenness property in metric spaces and its role in the quantitative analysis of the `Lion-Man' game. Pacific Journal of Mathematics, 310:181--212, 2021. DOI. |
| [75] | U. Kohlenbach and A. Sipoş. The finitary content of sunny nonexpansive retractions. Communications in Contemporary Mathematics, 23(1):1950093, 63pp., 2021. DOI. |
| [76] | U. Kohlenbach. Quantitative results on the Proximal Point Algorithm in uniformly convex Banach spaces. Journal of Convex Analysis, 28(1):11--18, 2021. |
| [77] | W. Simmons and H. Towsner. Explicit polynomial bounds on prime ideals in polynomial rings over fields. Pacific Journal of Mathematics, 306(2):721--754, 2020. DOI. |
| [78] | F. Ferreira. Bounds for indexes of nilpotency in commutative ring theory: A proof mining approach. Bulletin of Symbolic Logic, 26(3--4):257--267, 2020. DOI. |
| [79] | P. Engrácia and F. Ferreira. Bounded functional interpretation with an abstract type. In A. Rezuş, editor, Contemporary Logic and Computing, volume 1 of Landscapes in Logic, pages 87--112. College Publications, 2020. |
| [80] | T. Powell. On the computational content of Zorn's lemma. In Proceedings of LICS '20, pages 768--781. ACM, 2020. DOI. |
| [81] | T. Powell. A note on the finitization of Abelian and Tauberian theorems. Mathematical Logic Quarterly, 66(3):300--310, 2020. DOI. |
| [82] | B. Dinis and P. Pinto. Metastability of the multi-parameters proximal point algorithm. Portugaliae Mathematica, 77(3/4):345--381, 2020. DOI. |
| [83] | U. Kohlenbach. Quantitative analysis of a Halpern-type Proximal Point Algorithm for accretive operators in Banach spaces. Journal of Nonlinear and Convex Analysis, 21(9):2125--2138, 2020. LINK. |
| [84] | U. Kohlenbach and T. Powell. Rates of convergence for iterative solutions of equations involving set-valued accretive operators. Computers & Mathematics with Applications, 80:490--503, 2020. DOI. |
| [85] | U. Kohlenbach. Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. In P. Weingartner and H.-P. Leeb, editors, Kreisel's Interests. On the Foundations of Logic and Mathematics, volume 41 of Tributes, pages 45--61. College Publications, 2020. |
| [86] | W. Simmons and H. Towsner. Proof mining and effective bounds in differential polynomial rings. Advances in Mathematics, 343:567--623, 2019. DOI. |
| [87] | P. Pinto. Proof mining with the bounded functional interpretation. PhD thesis, Universidade de Lisboa, 2019. |
| [88] | T. Powell. A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces. Journal of Mathematical Analysis and Applications, 478(2):790--805, 2019. DOI. |
| [89] | T. Powell. A proof theoretic study of abstract termination principles. Journal of Logic and Computation, 29(8):1345--1366, 2019. DOI. |
| [90] | A. Sipoş. Proof mining in Lp-spaces. The Journal of Symbolic Logic, 84(4):1612--1629, 2019. DOI. |
| [91] | A. Sipoş. The asymptotic behaviour of convex combinations of firmly nonexpansive mappings. Journal of Convex Analysis, 26(3):911--924, 2019. |
| [92] | F. Ferreira, L. Leuştean, and P. Pinto. On the removal of weak compactness arguments in proof mining. Advances in Mathematics, 354:106728, 55pp., 2019. DOI. |
| [93] | U. Kohlenbach. Proof-theoretic Methods in Nonlinear Analysis. In B. Sirakov, P. Ney de Souza, and M. Viana, editors, Proceedings ICM 2018, volume 2, pages 61--82. World Scientific, 2019. DOI. |
| [94] | U. Kohlenbach. A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space. Foundations of Computational Mathematics, 19:83--99, 2019. DOI. |
| [95] | U. Kohlenbach, G. Lopez-Acedo, and A. Nicolae. Moduli of regularity and rates of convergence for Fejér monotone sequences. Israel Journal of Mathematics, 232:261--297, 2019. DOI. |
| [96] | A. Koutsoukou-Argyraki. New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups. Journal of Logic and Analysis, 10(7):1--30, 2018. DOI. |
| [97] | B. Dinis and J. Gaspar. Intuitionistic nonstandard bounded modified realisability and functional interpretation. Annals of Pure and Applied Logic, 169(5):392--412, 2018. DOI. |
| [98] | L. Leuştean, A. Nicolae, and A. Sipoş. An abstract proximal point algorithm. Journal of Global Optimization, 72(3):553--577, 2018. DOI. |
| [99] | L. Leuştean and A. Sipoş. Effective strong convergence of the proximal point algorithm in CAT(0) spaces. Journal of Nonlinear and Variational Analysis, 2(2):219--228, 2018. LINK. |
| [100] | L. Leuştean and A. Sipoş. An application of proof mining to the proximal point algorithm in CAT(0) spaces. In A. Bellow, C. Calude, and T. Zamfirescu, editors, Mathematics Almost Everywhere. In Memory of Solomon Marcus, pages 153--168. World Scientific, 2018. DOI. |
| [101] | M. Bacak and U. Kohlenbach. On proximal mappings with Young functions in uniformly convex Banach spaces. Journal of Convex Analysis, 25:1291--1318, 2018. |
| [102] | U. Kohlenbach, L. Leuştean, and A. Nicolae. Quantitative results on Fejér monotone sequences. Communications in Contemporary Mathematics, 20:42pp., 2018. DOI. |
| [103] | I. Goldbring, B. Hart, and H. Towsner. Explicit sentences distinguishing McDuff's II1 factors. arXiv preprint, arXiv:1701.07928, 2017. |
| [104] | A. Sipoş. Contributions to proof mining. PhD thesis, Universitatea din Bucureşti, 2017. |
| [105] | A. Koutsoukou-Argyraki. Effective rates of convergence for the resolvents of accretive operators. Numerical Functional Analysis and Optimization, 38(12):1601--1613, 2017. DOI. |
| [106] | L. Leuştean and A. Nicolae. A note on an alternative iterative method for nonexpansive mappings. Journal of Convex Analysis, 24:501--503, 2017. |
| [107] | A. Sipoş. A note on the Mann iteration for k-strict pseudocontractions in Banach spaces. Numerical Functional Analysis and Optimization, 38(1):80--90, 2017. DOI. |
| [108] | A. Sipoş. Effective results on a fixed point algorithm for families of nonlinear mappings. Annals of Pure and Applied Logic, 168(1):112--128, 2017. DOI. |
| [109] | U. Kohlenbach and A. Nicolae. A proof-theoretic bound extraction theorem for CAT(κ)-spaces. Studia Logica, 105:611--624, 2017. DOI. |
| [110] | U. Kohlenbach. Recent progress in proof mining in nonlinear analysis. IFCoLog Journal of Logics and their Applications, 10(4):3361--3410, 2017. |
| [111] | U. Kohlenbach, G. López-Acedo, and A. Nicolae. Quantitative asymptotic regularity results for the composition of two mappings. Optimization, 66:1291--1299, 2017. DOI. |
| [112] | H. Towsner. Towards an effective theory of absolutely continuous measures. In P. Cégielski, A. Enayat, and R. Kossak, editors, Studies in Weak Arithmetics. Vol. 3, volume 217 of CSLI Lecture Notes, pages 171--229. CSLI Publications, Stanford, CA, 2016. |
| [113] | A. Koutsoukou-Argyraki. Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups. PhD thesis, TU Darmstadt, 2016. |
| [114] | D. Körnlein. Quantitative Analysis of Iterative Algorithms in Fixed Point Theory and Convex Optimization. PhD thesis, TU Darmstadt, 2016. |
| [115] | D. Körnlein. Quantitative strong convergence for the hybrid steepest descent method. arXiv preprint, arXiv:1610.00517, 2016. |
| [116] | D. Körnlein. Quantitative results for Bruck iterations of demicontinuous pseudocontractions. arXiv preprint, arXiv:1610.00515, 2016. |
| [117] | L. Leuştean, V. Radu, and A. Sipoş. Quantitative results on the Ishikawa iteration of Lipschitz pseudo-contractions. Journal of Nonlinear and Convex Analysis, 17(11):2277--2292, 2016. LINK. |
| [118] | L. Leuştean and A. Nicolae. Effective results on nonlinear ergodic averages in CAT(k) spaces. Ergodic Theory and Dynamical Systems, 36:2580--2601, 2016. DOI. |
| [119] | U. Kohlenbach and A. Koutsoukou-Argyraki. Effective asymptotic regularity for one-parameter nonexpansive semigroups. Journal of Mathematical Analysis and Applications, 433:1883--1903, 2016. DOI. |
| [120] | U. Kohlenbach. On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces. Israel Journal of Mathematics, 216:215--246, 2016. DOI. |
| [121] | D. Günzel and U. Kohlenbach. Logical metatheorems for abstract spaces axiomatized in positive bounded logic. Advances in Mathematics, 290:503--551, 2016. DOI. |
| [122] | P. Oliva and T. Powell. A game-theoretic computational interpretation of proofs in classical analysis. In R. Kahle and M. Rathjen, editors, Gentzen's Centenary: The Quest for Consistency, pages 501--531. Springer, 2015. DOI. |
| [123] | P. Oliva and T. Powell. A constructive interpretation of Ramsey's theorem via the product of selection functions. Mathematical Structure in Computer Science, 25(8):1755--1778, 2015. DOI. |
| [124] | A. Kreuzer. Measure theory and higher order arithmetic. Proceedings of the American Mathematical Society, 143:5411--5425, 2015. DOI. |
| [125] | H. Towsner. An Inverse Ackermannian Lower Bound on the Local Unconditionality Constant of the James Space. arXiv preprint, arXiv:1503.04745, 2015. |
| [126] | G. Moser and T. Powell. On the computational content of termination proofs. In Proceedings of CiE '15, pages 276--285, 2015. DOI. |
| [127] | D. Körnlein. Quantitative results for Halpern iterations of nonexpansive mappings. Journal of Mathematical Analysis and Applications, 428(2):1161--1172, 2015. DOI. |
| [128] | F. Ferreira and J. Gaspar. Nonstandardness and the bounded functional interpretation. Annals of Pure and Applied Logic, 166(6):701--712, 2015. DOI. |
| [129] | D. Ivan and L. Leuştean. A rate of asymptotic regularity for the Mann iteration of k-strict pseudo-contractions. Numerical Functional Analysis and Optimization, 36:792--798, 2015. DOI. |
| [130] | L. Leuştean and A. Nicolae. A note on an ergodic theorem in weakly uniformly convex geodesic spaces. Archiv der Mathematik, 105:467--477, 2015. DOI. |
| [131] | U. Kohlenbach and A. Koutsoukou-Argyraki. Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators. Journal of Mathematical Analysis and Applications, 423:1089--1112, 2015. DOI. |
| [132] | J. Avigad and J. Rute. Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory and Dynamical Systems, 35:1009--1027, 2015. DOI. |
| [133] | L. Leuştean and A. Nicolae. Effective results on compositions of nonexpansive mappings. Journal of Mathematical Analysis and Applications, 410:902--907, 2014. DOI. |
| [134] | D. Ariza-Ruiz, L. Leuştean, and G. Lopez-Acedo. Firmly nonexpansive mappings in classes of geodesic spaces. Transactions of the American Mathematical Society, 366:4299--4322, 2014. DOI. |
| [135] | M.A.A. Khan and U. Kohlenbach. Quantitative image recovery theorems. Nonlinear Analysis: Theory, Methods & Applications, 106:138--150, 2014. DOI. |
| [136] | U. Kohlenbach and D. Körnlein. Rate of metastability for Bruck's iteration of pseudocontractive mappings in Hilbert space. Numerical Functional Analysis and Optimization, 35:20--31, 2014. DOI. |
| [137] | L. Leuştean. An application of proof mining to nonlinear iterations. Annals of Pure and Applied Logic, 165:1484--1500, 2014. DOI. |
| [138] | U. Kohlenbach and P. Safarik. Fluctuations, effective learnability and metastability in analysis. Annals of Pure and Applied Logic, 165:266--304, 2014. DOI. |
| [139] | H. Towsner. Partial impredicativity in reverse mathematics. The Journal of Symbolic Logic, 78(2):459--488, 2013. DOI. |
| [140] | T. Powell. On Bar Recursive Interpretations of Analysis. PhD thesis, Queen Mary University of London, 2013. |
| [141] | A. Kreuzer. Program extraction for 2-random reals. Archive for Mathematical Logic, 52(5--6):659--666, 2013. DOI. |
| [142] | A. Nicolae. Asymptotic behavior of averaged and firmly nonexpansive mappings in geodesic spaces. Nonlinear Analysis: Theory, Methods & Applications, 87:102--115, 2013. DOI. |
| [143] | P. Safarik. On the extraction of computational content from noneffective convergence proofs in analysis. PhD thesis, TU Darmstadt, 2013. |
| [144] | D. Ariza-Ruiz, E.M. Briseid, A. Jiménez-Melado, and G. López-Acedo. Rate of convergence under weak contractiveness conditions. Fixed Point Theory, 14(1):11--28, 2013. |
| [145] | M.A.A. Khan and U. Kohlenbach. Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces. Journal of Mathematical Analysis and Applications, 403:633--642, 2013. DOI. |
| [146] | A. Kreuzer. A logical analysis of the generalized Banach contractions principle. Journal of Logic and Analysis, 4(17):1--16, 2012. DOI. |
| [147] | A. Kreuzer. Non-principal ultrafilters, program extraction and higher order reverse mathematics. Journal of Mathematical Logic, 12(1):1250002, 16pp., 2012. DOI. |
| [148] | J. Avigad, E.T. Dean, and J. Rute. A metastable dominated convergence theorem. Journal of Logic and Analysis, 4(3):1--19, 2012. DOI. |
| [149] | A.P. Kreuzer. Proof mining and combinatorics: Program extraction for Ramsey's theorem for pairs. PhD thesis, TU Darmstadt, 2012. |
| [150] | G. Ferreira and P. Oliva. On bounded functional interpretations. Annals of Pure and Applied Logic, 163(8):1030--1049, 2012. DOI. |
| [151] | T. Powell. Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's Lemma. In Proceedings of CL&C '12, pages 49--62, 2012. DOI. |
| [152] | K. Schade and U. Kohlenbach. Effective metastability for modified Halpern iterations in CAT(0) spaces. Fixed Point Theory and Applications, 191:19pp., 2012. DOI. |
| [153] | U. Kohlenbach and L. Leuştean. On the computational content of convergence proofs via Banach limits. Philosophical Transactions of the Royal Society A, 370(1971):3449--3463, 2012. DOI. |
| [154] | U. Kohlenbach and A.P. Kreuzer. Term extraction and Ramsey's theorem for pairs. The Journal of Symbolic Logic, 77:853--895, 2012. DOI. |
| [155] | U. Kohlenbach. A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Communications in Contemporary Mathematics, 14:20pp., 2012. DOI. |
| [156] | U. Kohlenbach. Gödel functional interpretation and weak compactness. Annals of Pure and Applied Logic, 163:1560--1579, 2012. DOI. |
| [157] | P. Safarik. A quantitative nonlinear strong ergodic theorem for Hilbert spaces. Journal of Mathematical Analysis and Applications, 391:26--37, 2012. DOI. |
| [158] | U. Kohlenbach and L. Leuştean. Effective metastability of Halpern iterates in CAT(0) spaces. Advances in Mathematics, 231:2526--2556, 2012. DOI. |
| [159] | G. Kreisel. Logical Hygiene, Foundations, and Abstractions: Diversity among Aspects and Options. In M. Baaz, C.H. Papadimitriou, H.W. Putnam, D.S. Scott, and C.L. Harper Jr., editors, Kurt Gödel and the Foundations of Mathematics. Horizons of Truth, pages 27--53. Cambridge University Press, New York, 2011. DOI. |
| [160] | J. Gaspar. Proof interpretations: theoretical and practical aspects. PhD thesis, TU Darmstadt, 2011. |
| [161] | V. Colao, L. Leuştean, G. Lopez-Acedo, and V. Martin-Marquez. Alternative iterative methods for nonexpansive mappings, rates of convergence and application. Journal of Convex Analysis, 18:465--487, 2011. |
| [162] | U. Kohlenbach. On the asymptotic behavior of odd operators. Journal of Mathematical Analysis and Applications, 382:615--620, 2011. DOI. |
| [163] | U. Kohlenbach. A note on the monotone functional interpretation. Mathematical Logic Quarterly, 57:611--614, 2011. DOI. |
| [164] | D. Körnlein and U. Kohlenbach. Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces. Nonlinear Analysis: Theory, Methods & Applications, 74:5253--5267, 2011. DOI. |
| [165] | U. Kohlenbach. Gödel's functional interpretation and its use in current mathematics. In M. Baaz, C.H. Papadimitriou, H.W. Putnam, D.S. Scott, and C.L. Harper Jr., editors, Kurt Gödel and the Foundations of Mathematics. Horizons of Truth, pages 361--398. Cambridge University Press, New York, 2011. DOI. |
| [166] | U. Kohlenbach. On quantitative versions of theorems due to F.E. Browder and R. Wittmann. Advances in Mathematics, 226:2764--2795, 2011. DOI. |
| [167] | J. Avigad and H. Towsner. Metastability in the Furstenberg-Zimmer tower. Fundamenta Mathematicae, 210(3):243--268, 2010. DOI. |
| [168] | E.M. Briseid. A new uniformity for asymptotic contractions in the sense of Kirk. International Journal of Mathematics and Statistics, 6:2--13, 2010. |
| [169] | P. Engrácia and F. Ferreira. The bounded functional interpretation of the double negation shift. The Journal of Symbolic Logic, 75(2):759--773, 2010. DOI. |
| [170] | J. Gaspar and P. Oliva. Proof interpretations with truth. Mathematical Logic Quarterly, 56(6):591--610, 2010. DOI. |
| [171] | L. Leuştean. Nonexpansive iterations in uniformly convex W-hyperbolic spaces. In A. Leizarowitz, B.S. Mordukhovich, I. Shafrir, and A. Zaslavski, editors, Nonlinear Analysis and Optimization I: Nonlinear Analysis, volume 513 of Contemporary Mathematics, pages 193--209. American Mathematical Society, 2010. |
| [172] | U. Kohlenbach and P. Safarik. On the computational content of the Bolzano-Weierstrass principle. Mathematical Logic Quaterly, 56:508--532, 2010. DOI. |
| [173] | U. Kohlenbach. On the logical analysis of proofs based on nonseparable Hilbert space theory. In S. Feferman and W. Sieg, editors, Proofs, Categories and Computations. Essays in Honor of Grigori Mints, pages 131--143. College Publications, 2010. |
| [174] | J. Gaspar and U. Kohlenbach. On Tao's "finitary" infinite pigeonhole principle. The Journal of Symbolic Logic, 75:355--371, 2010. DOI. |
| [175] | U. Kohlenbach and L. Leuştean. Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces. Journal of the European Mathematical Society, 12:71--92, 2010. DOI. |
| [176] | J. Avigad, P. Gerhardy, and H. Towsner. Local stability of ergodic averages. Transactions of the American Mathematical Society, 362:261--288, 2010. DOI. |
| [177] | H. Towsner. Metastability and the Furstenberg-Zimmer Tower II: Polynomial and Multidimensional Szemeredi's Theorem. arXiv preprint, arXiv:0909.5668, 2009. |
| [178] | J. Avigad. The metamathematics of ergodic theory. Annals of Pure and Applied Logic, 157(2--3):64--76, 2009. DOI. |
| [179] | P. Engrácia. Proof-theoretic studies on the bounded functional interpretation. PhD thesis, Universidade de Lisboa, 2009. |
| [180] | F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157(2--3):122--129, 2009. DOI. |
| [181] | E.M. Briseid. On Rates of Convergence in Metric Fixed Point Theory. PhD thesis, TU Darmstadt, 2009. |
| [182] | J. Gaspar. Factorization of the Shoenfield-like bounded functional interpretation. Notre Dame Journal of Formal Logic, 50(1):53--60, 2009. DOI. |
| [183] | U. Kohlenbach and A. Kreuzer. Ramsey's theorem for pairs and provably recursive functions. Notre Dame Journal of Formal Logic, 50:427--444, 2009. DOI. |
| [184] | U. Kohlenbach and L. Leuştean. A quantitative mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory and Dynamical Systems, 29:1907--1915, 2009. DOI. |
| [185] | E.M. Briseid. Logical aspects of rates of convergence in metric spaces. The Journal of Symbolic Logic, 74:1401--1428, 2009. DOI. |
| [186] | E.M. Briseid. Fixed points of generalized contractive mappings. Journal of Nonlinear and Convex Analysis, 9(2):181--204, 2008. |
| [187] | P. Gerhardy. Proof mining in topological dynamics. Notre Dame Journal of Formal Logic, 49:431--446, 2008. DOI. |
| [188] | T. Tao. Soft analysis, hard analysis, and the finite convergence principle. In Structure and Randomness: Pages from Year One of a Mathematical Blog. AMS, 2008. |
| [189] | U. Kohlenbach. Herbrand's theorem and extractive proof theory. SMF - Gazette des Mathematiciens, 118:29--41, 2008. |
| [190] | U. Kohlenbach. Effective uniform bounds from proofs in abstract functional analysis. In B. Cooper, B. Loewe, and A. Sorbi, editors, New Computational Paradigms: Changing Conceptions of What is Computable, pages 223--258. Springer Publisher, 2008. DOI. |
| [191] | U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer Heidelberg-Berlin, 2008. DOI. |
| [192] | P. Gerhardy and U. Kohlenbach. General logical metatheorems for functional analysis. Transactions of the American Mathematical Society, 360:2615--2660, 2008. DOI. |
| [193] | E.M. Briseid. Some results on Kirk's asymptotic contractions. Fixed Point Theory, 8(1):17--27, 2007. |
| [194] | F. Ferreira and P. Oliva. Bounded functional interpretation and feasible analysis. Annals of Pure and Applied Logic, 145(2):115--129, 2007. DOI. |
| [195] | E.M. Briseid. A rate of convergence for asymptotic contractions. Journal of Mathematical Analysis and Applications, 330(1):364--376, 2007. DOI. |
| [196] | L. Leuştean. A quadratic rate of asymptotic regularity for CAT(0)-spaces. Journal of Mathematical Analysis and Applications, 325:386--399, 2007. DOI. |
| [197] | L. Leuştean. Rates of asymptotic regularity for Halpern iterations of nonexpansive mappings. Journal of Universal Computer Science, 13:1680--1691, 2007. |
| [198] | U. Kohlenbach. Proof interpretations and the computational content of proofs in mathematics. Bulletin EATCS, 93:143--173, 2007. |
| [199] | U. Kohlenbach and L. Leuştean. The approximate fixed point property in product spaces. Nonlinear Analysis: Theory, Methods & Applications, 66:806--818, 2007. DOI. |
| [200] | B. Lambov. Topics in the Theory and Practice of Computable Analysis. PhD thesis, University of Aarhus, 2006. DOI. |
| [201] | P. Gerhardy. Applications of Proof Interpretations. PhD thesis, University of Aarhus, 2006. |
| [202] | P. Gerhardy. A quantitative version of Kirk's fixed point theorem for asymptotic contractions. Journal of Mathematical Analysis and Applications, 316(1):339--345, 2006. DOI. |
| [203] | L. Leuştean. Proof mining in R-trees and hyperbolic spaces. Electronic Notes in Theoretical Computer Science, 165:95--106, 2006. DOI. |
| [204] | U. Kohlenbach. A logical uniform boundedness principle for abstract metric and hyperbolic spaces. Electronic Notes in Theoretical Computer Science, 165:81--93, 2006. DOI. |
| [205] | P. Gerhardy and U. Kohlenbach. Strongly uniform bounds from semi-constructive proofs. Annals of Pure and Applied Logic, 141:89--107, 2006. DOI. |
| [206] | A. Macintyre. The mathematical significance of proof theory. Philosophical Transactions of the Royal Society A, 363(1835):2419--2435, 2005. DOI. |
| [207] | F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135(1--3):73--112, 2005. DOI. |
| [208] | B. Lambov. Rates of convergence of recursively defined sequences. Electronic Notes in Theoretical Computer Science, 120:125--133, 2005. DOI. |
| [209] | U. Kohlenbach. Some computational aspects of metric fixed point theory. Nonlinear Analysis: Theory, Methods & Applications, 61:823--837, 2005. DOI. |
| [210] | U. Kohlenbach. Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society, 357(1):89--128, 2005. DOI. |
| [211] | U. Kohlenbach and B. Lambov. Bounds on iterations of asymptotically quasi-nonexpansive mappings. In G.J. Falset, E.L. Fuster, and B. Sims, editors, Proceedings of the International Conference on Fixed Point Theory, Valencia 2003, pages 143--172. Yokohama Press, 2004. LINK. |
| [212] | P. Oliva. Proof Mining in Subsystems of Analysis. PhD thesis, University of Aarhus, 2003. |
| [213] | P. Oliva. Polynomial-time algorithms from ineffective proofs. In 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pages 128--137, 2003. DOI. |
| [214] | U. Kohlenbach and P. Oliva. Proof mining: a systematic way of analysing proofs in mathematics. Proceedings of the Steklov Institute of Mathematics, 242:136--164, 2003. |
| [215] | U. Kohlenbach and L. Leuştean. Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Abstract and Applied Analysis, 2003(8):449--477, 2003. DOI. |
| [216] | U. Kohlenbach. Uniform asymptotic regularity for Mann iterates. Journal of Mathematical Analysis and Applications, 279:531--544, 2003. DOI. |
| [217] | U. Kohlenbach and P. Oliva. Proof mining in L1-approximation. Annals of Pure and Applied Logic, 121:1--38, 2003. DOI. |
| [218] | P. Oliva. On the computational complexity of L1-approximation. Mathematical Logic Quarterly, 48(66--77):1, 2002. DOI. |
| [219] | U. Kohlenbach. Applied foundations: proof mining in analysis. Newsletter of the Danish Mathematical Society (`Matilde'), 13:7--9, 2002. |
| [220] | U. Kohlenbach. Foundational and mathematical uses of higher types. In W. Sieg, R. Sommer, and C. Talcott, editors, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, volume 15 of Lecture Notes in Logic, pages 92--116. A.K. Peters, 2002. |
| [221] | U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numerical Functional Analysis and Optimization, 22:641--656, 2001. DOI. |
| [222] | U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In J. Blanck, V. Brattka, P. Hertling, and K. Weihrauch, editors, Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, volume 2064 of Lecture Notes in Computer Science, pages 119--145. Springer Berlin Heidelberg, 2001. DOI. |
| [223] | U. Kohlenbach. Things that can and things that can't be done in PRA. Annals of Pure and Applied Logic, 102:223--245, 2000. DOI. |
| [224] | M. Baaz. Note on the generalization of calculations. Theoretical Computer Science, 224(1--2):3--11, 1999. DOI. |
| [225] | U. Kohlenbach. The use of a logical principle of uniform boundedness in analysis. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundations of Mathematics, volume 280 of Synthese Library, pages 93--106. Kluwer Academic Publishers, 1999. DOI. |
| [226] | U. Kohlenbach. On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. Annals of Pure and Applied Logic, 95:257--285, 1998. DOI. |
| [227] | U. Kohlenbach. Relative constructivity. The Journal of Symbolic Logic, 63:1218--1238, 1998. DOI. |
| [228] | U. Kohlenbach. Proof theory and computational analysis. Electronic Notes in Theoretical Computer Science, 13:124--157, 1998. DOI. |
| [229] | U. Kohlenbach. Arithmetizing proofs in analysis. In J.M. Larrazabal, D. Lascar, and G. Mints, editors, Logic Colloquium '96, volume 12 of Springer Lecture Notes in Logic, pages 115--158. Springer Berlin Heidelberg, 1998. |
| [230] | U. Kohlenbach. Elimination of Skolem functions for monotone formulas in analysis. Archive for Mathematical Logic, 37:363--390, 1998. DOI. |
| [231] | C.N. Delzell. Kreisel's Unwinding of Artin's Proof. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 113--246. A.K. Peters, Wellesley Massachusetts, 1996. |
| [232] | H. Luckhardt. Bounds Extracted by Kreisel from Ineffective Proofs. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 289--300. A.K. Peters, Wellesley Massachusetts, 1996. |
| [233] | S. Feferman. Kreisel's `Unwinding Program'. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 247--273. A.K. Peters, Wellesley Massachusetts, 1996. |
| [234] | U. Kohlenbach. Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals. Archive for Mathematical Logic, 36:31--71, 1996. DOI. |
| [235] | U. Kohlenbach. Analysing proofs in analysis. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pages 225--260. Oxford University Press, 1996. |
| [236] | U. Kohlenbach. New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization, 14:581--606, 1993. DOI. |
| [237] | U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic, 64:27--94, 1993. DOI. |
| [238] | U. Kohlenbach. Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. The Journal of Symbolic Logic, 57:1239--1273, 1992. DOI. |
| [239] | G. Bellin. Ramsey interpreted: a parametric version of Ramsey's theorem. In Logic and computation (Pittsburgh, PA, 1987), volume 106 of Contemporary Mathematics, pages 17--37. American Mathematical Society, Providence, RI,, 1990. |
| [240] | G. Kreisel. Logical aspects of computation: contributions and distractions. In P. Odifreddi, editor, Logic and Computer Science, pages 205--278. Academic Press, London, 1990. |
| [241] | U. Kohlenbach. Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen. PhD thesis, Johann Wolfgang Goethe-Universität Frankfurt am Main, 1990. |
| [242] | H. Luckhardt. Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. The Journal of Symbolic Logic, 54:234--263, 1989. DOI. |
| [243] | G. Kreisel. Proof Theory and Synthesis of Programs: Potentials and Limitations. In B. Buchberger, editor, Eurocal ’85 (Linz 1985), volume 203 of Lecture Notes in Computer Science, pages 136--150. Springer, 1986. DOI. |
| [244] | M.J. Beeson. Foundations of Constructive Mathematics. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer Berlin, Heidelberg, 1985. DOI. |
| [245] | G. Kreisel and A. Macintyre. Constructive logic versus algebraization I. In A.S. Troelstra and D. van Dalen, editors, Proceedings L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), pages 217--260. North-Holland, Amsterdam, 1982. DOI. |
| [246] | G. Kreisel. Finiteness theorems in arithmetic: an application of Herbrand’s theorem for Σ2-formulas. In Proceedings of the Herbrand symposium (Marseille, 1981), pages 39--55. North-Holland, Amsterdam, 1982. DOI. |
| [247] | M.J. Beeson. Principles of continuous choice and continuity of functions in formal systems for constructive mathematics. Annals of Mathematical Logic, 12:249--322, 1977. DOI. |
| [248] | J.-Y. Girard. The ordinal ε0 and arithmetic. In Proof Theory and Logical Complexity, volume 1 of Studies in Proof Theory, pages 411--496. Bibliopolis, 1977. |
| [249] | A.S. Troelstra. Aspects of constructive mathematics. In J. Barwise, editor, Handbook of Mathematical Logic, pages 973--1052. North-Holland, Amsterdam, 1977. DOI. |
| [250] | G. Kreisel. On the kind of data needed for a theory of proofs. In R. Gandy and M. Hyland, editors, Logic Colloquium 76, pages 111--128. North-Holland Publishing Company, 1977. DOI. |
| [251] | G. Kreisel. What have we learnt from Hilbert's second problem? In F.E. Browder, editor, Mathematical developments arising from Hilbert problems, volume 28 of Proceedings of Symposia in Pure Mathematics, pages 93--130. AMS, 1976. |
| [252] | G. Kreisel. Der unheilvolle Einbruch der Logik in die Mathematik. Acta Philosophica Fennica, 28:166--187, 1976. |
| [253] | G. Kreisel. Hilbert's programme and the search for automatic proof procedures. In M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Symposium on Automatic Deduction, volume 125 of Lecture Notes in Mathematics, pages 128--146. Springer, 1970. DOI. |
| [254] | E. Bishop. Mathematics as a Numerical Language. In A. Kino, J. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y., pages 53--71. North-Holland, Amsterdam, 1968. DOI. |
| [255] | G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101--128. North-Holland, Amsterdam, 1959. |
| [256] | G. Kreisel. Mathematical significance of consistency proofs. The Journal of Symbolic Logic, 23:155--182, 1958. DOI. |
| [257] | G. Kreisel. On the interpretation of non-finitist proofs, part II. The Journal of Symbolic Logic, 17:43--58, 1952. DOI. |
| [258] | G. Kreisel. On the interpretation of non-finitist proofs, part I. The Journal of Symbolic Logic, 16:241--267, 1951. DOI. |
This file was generated by bibtex2html 1.99.