{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:05:45Z","timestamp":1725566745560},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540282310"},{"type":"electronic","value":"9783540318972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_33","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T09:35:33Z","timestamp":1127813733000},"page":"477-492","source":"Crossref","is-referenced-by-count":3,"title":["Light Functional Interpretation"],"prefix":"10.1007","author":[{"given":"Mircea-Dan","family":"Hernest","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"33_CR1","doi-asserted-by":"publisher","first-page":"1785","DOI":"10.2307\/2695075","volume":"65","author":"J. Avigad","year":"2000","unstructured":"Avigad, J.: Interpreting classical theories in constructive ones. The Journal of Symbolic Logic\u00a065(4), 1785\u20131812 (2000)","journal-title":"The Journal of Symbolic Logic"},{"key":"33_CR2","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0049-237X(98)80020-7","volume-title":"Handbook of Proof Theory","author":"J. Avigad","year":"1998","unstructured":"Avigad, J., Feferman, S.: G\u00f6del\u2019s functional (\u2018Dialectica\u2019) interpretation. In: Buss, S.R. (ed.) Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a0137, pp. 337\u2013405. Elsevier, Amsterdam (1998)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0037097","volume-title":"Typed Lambda Calculi and Applications","author":"F. Barbanera","year":"1993","unstructured":"Barbanera, F., Berardi, S.: Extracting constructive content from classical logic via control\u2013like reductions. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 45\u201359. Springer, Heidelberg (1993)"},{"issue":"1","key":"33_CR4","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J.L. Bates","year":"1985","unstructured":"Bates, J.L., Constable, R.L.: Proofs as programs. ACM Transactions on Programming Languages and Systems\u00a07(1), 113\u2013136 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1-3","key":"33_CR5","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.apal.2004.10.006","volume":"133","author":"U. Berger","year":"2005","unstructured":"Berger, U.: Uniform Heyting Arithmetic. Annals of Pure and Applied Logic\u00a0133(1-3), 125\u2013148 (2005); Festschrift for H. Schwichtenberg\u2019s 60th birthday","journal-title":"Annals of Pure and Applied Logic"},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0168-0072(01)00073-2","volume":"114","author":"U. Berger","year":"2002","unstructured":"Berger, U., Buchholz, W., Schwichtenberg, H.: Refined program extraction from classical proofs. Annals of Pure and Applied Logic\u00a0114, 3\u201325 (2002)","journal-title":"Annals of Pure and Applied Logic"},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1026748613865","volume":"26","author":"U. Berger","year":"2001","unstructured":"Berger, U., Schwichtenberg, H., Seisenberger, M.: The Warshall algorithm and Dickson\u2019s lemma: Two examples of realistic program extraction. Journal of Automated Reasoning\u00a026, 205\u2013221 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR8","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1017\/CBO9780511569807.014","volume-title":"Logical Frameworks","author":"R.L. Constable","year":"1991","unstructured":"Constable, R.L., Murthy, C.: Finding computational content in classical proofs. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 341\u2013362. Cambridge University Press, Cambridge (1991)"},{"issue":"4","key":"33_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1017\/S0960129599002844","volume":"9","author":"T. Coquand","year":"1999","unstructured":"Coquand, T., Hofmann, M.: A new method for establishing conservativity of classical systems over their intuitionistic version. Mathematical Structures in Computer Science\u00a09(4), 323\u2013333 (1999)","journal-title":"Mathematical Structures in Computer Science"},{"key":"33_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF02025118","volume":"16","author":"J. Diller","year":"1974","unstructured":"Diller, J., Nahm, W.: Eine Variante zur Dialectica Interpretation der Heyting Arithmetik endlicher Typen. Archiv f\u00fcr Mathematische Logik und Grundlagenforschung\u00a016, 49\u201366 (1974)","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"33_CR11","unstructured":"Ferreira, F., Oliva, P.: Bounded Functional Interpretation. Annals of Pure and Applied Logic, 48 pp., see Elseviers\u2019s Science Direct on the Internet (to appear)"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","first-page":"21","volume-title":"Mathematics of Program Construction","author":"H. Friedman","year":"1993","unstructured":"Friedman, H.: Classical and intuitionistically provably recursive functions. In: Bird, R.S., Woodcock, J.C.P., Morgan, C.C. (eds.) MPC 1992. LNCS, vol.\u00a0669, pp. 21\u201327. Springer, Heidelberg (1993)"},{"key":"33_CR13","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"G\u00f6del, K.: \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. Dialectica\u00a012, 280\u2013287 (1958)","journal-title":"Dialectica"},{"key":"33_CR14","unstructured":"Hernest, M.-D.: Technical Appendix to this paper. See the author\u2019s web-page"},{"key":"33_CR15","series-title":"Kurt G\u00f6del Society\u2019s Collegium Logicum","first-page":"99","volume-title":"CSL 2003: Extended Posters","author":"M.-D. Hernest","year":"2004","unstructured":"Hernest, M.-D.: A comparison between two techniques of program extraction from classical proofs. In: Baaz, M., Makovsky, J., Voronkov, A. (eds.) CSL 2003. Kurt G\u00f6del Society\u2019s Collegium Logicum, vol.\u00a0VIII, pp. 99\u2013102. Springer, Heidelberg (2004)"},{"issue":"1-3","key":"33_CR16","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.tcs.2004.12.019","volume":"338","author":"M.-D. Hernest","year":"2005","unstructured":"Hernest, M.-D., Kohlenbach, U.: A complexity analysis of functional interpretations. Theoretical Computer Science\u00a0338(1-3), 200\u2013246 (2005)","journal-title":"Theoretical Computer Science"},{"key":"33_CR17","unstructured":"Howard, W.A.: Hereditarily majorizable functionals of finite type. In: [38], pp. 454\u2013461"},{"key":"33_CR18","first-page":"119","volume":"4","author":"I. Johansson","year":"1936","unstructured":"Johansson, I.: Der Minimalkalk\u00fcl, ein reduzierter intuitionistischer Formalismus. Compositio Matematica\u00a04, 119\u2013136 (1936)","journal-title":"Compositio Matematica"},{"key":"33_CR19","unstructured":"J\u00f8rgensen, K.F.: Finite type arithmetic. Master\u2019s thesis, Departments of Mathematics and Philosophy, University of Roskilde, Roskilde, Denmark (2001)"},{"key":"33_CR20","unstructured":"Kohlenbach, U.: Proof Interpretations and the Computational Content of Proofs. Lecture Course, latest version in the author\u2019s web page"},{"key":"33_CR21","series-title":"European Logic Colloquium","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1093\/oso\/9780198538622.003.0010","volume-title":"Logic: from Foundations to Applications","author":"U. Kohlenbach","year":"1996","unstructured":"Kohlenbach, U.: Analysing proofs in Analysis. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: from Foundations to Applications, Keele, 1993. European Logic Colloquium, pp. 225\u2013260. Oxford University Press, Oxford (1996)"},{"key":"33_CR22","first-page":"136","volume":"242","author":"U. Kohlenbach","year":"2003","unstructured":"Kohlenbach, U., Oliva, P.: Proof mining: a systematic way of analysing proofs in Mathematics. Proc. of the Steklov Institute of Mathematics\u00a0242, 136\u2013164 (2003)","journal-title":"Proc. of the Steklov Institute of Mathematics"},{"key":"33_CR23","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101\u2013128. North-Holland Publishing Company, Amsterdam (1959)"},{"key":"33_CR24","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0168-0072(94)90047-7","volume":"68","author":"J.-L. Krivine","year":"1994","unstructured":"Krivine, J.-L.: Classical logic, storage operators and second-order lambda-calculus. Annals of Pure and Applied Logic\u00a068, 53\u201378 (1994)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"33_CR25","doi-asserted-by":"publisher","first-page":"682","DOI":"10.2307\/2274322","volume":"50","author":"D. Leivant","year":"1985","unstructured":"Leivant, D.: Syntactic translations and provably recursive functions. The Journal of Symbolic Logic\u00a050(3), 682\u2013688 (1985)","journal-title":"The Journal of Symbolic Logic"},{"key":"33_CR26","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0060871","volume-title":"Extensional G\u00f6del Functional Interpretation","author":"H. Luckhardt","year":"1973","unstructured":"Luckhardt, H.: Extensional G\u00f6del Functional Interpretation. Lecture Notes in Mathematics, vol.\u00a0306. Springer, Heidelberg (1973)"},{"key":"33_CR27","first-page":"289","volume-title":"Kreiseliana: About and around Georg Kreisel","author":"H. Luckhardt","year":"1996","unstructured":"Luckhardt, H.: Bounds extracted by Kreisel from ineffective proofs. In: Odifreddi, P. (ed.) Kreiseliana: About and around Georg Kreisel, pp. 289\u2013300. A.K. Peters, Wellesley (1996)"},{"key":"33_CR28","unstructured":"Murthy, C.: Extracting constructive content from classical proofs. Tech. Report 90\u2013 1151, Dep.of Comp.Science, Cornell Univ., Ithaca, NY, U.S.A, PhD thesis (1990)"},{"issue":"1-3","key":"33_CR29","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/j.apal.2004.10.012","volume":"133","author":"G.E. Ostrin","year":"2005","unstructured":"Ostrin, G.E., Wainer, S.S.: Elementary arithmetic. Annals of Pure and Applied Logic\u00a0133(1-3), 275\u2013292 (2005); Festschrift for H. Schwichtenberg\u2019s 60s","journal-title":"Annals of Pure and Applied Logic"},{"key":"33_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc\u2013calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"issue":"5\/6","key":"33_CR31","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. Journal of Symbolic Computation\u00a015(5\/6), 607\u2013640 (1993)","journal-title":"Journal of Symbolic Computation"},{"issue":"1-3","key":"33_CR32","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.tcs.2004.03.006","volume":"323","author":"C. Raffalli","year":"2004","unstructured":"Raffalli, C.: Getting results from programs extracted from classical proofs. Theoretical Computer Science\u00a0323(1-3), 49\u201370 (2004)","journal-title":"Theoretical Computer Science"},{"key":"33_CR33","unstructured":"Rath, P.: Eine verallgemeinerte Funktionalinterpretation der Heyting Arithmetik endlicher Typen. PhD thesis, Universit\u00e4t M\u00fcnster, Germany (1978)"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H.: Minimal logic for computable functions. Lecture course on program-extraction from (classical) proofs. Author\u2019s page or Minlog distrib. In: [36]","DOI":"10.1007\/978-3-642-58041-3_8"},{"key":"33_CR35","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1023\/A:1026459821186","volume":"62","author":"H. Schwichtenberg","year":"1999","unstructured":"Schwichtenberg, H.: Monotone majorizable functionals. Studia Logica\u00a062, 283\u2013289 (1999)","journal-title":"Studia Logica"},{"key":"33_CR36","unstructured":"Schwichtenberg, H., et al.: Proof- and program-extraction system Minlog, Free code and documentation at http:\/\/www.minlog-system.de"},{"key":"33_CR37","unstructured":"Stein, M.: Interpretation der Heyting-Arithmetik endlicher Typen. PhD thesis, Universit \u00e4t M\u00fcnster, Germany (1976)"},{"key":"33_CR38","series-title":"Lecture Notes in Mathematics","volume-title":"Metamathematical investigation of intuitionistic Arithmetic and Analysis","year":"1973","unstructured":"Troelstra, A.S. (ed.): Metamathematical investigation of intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol.\u00a0344. Springer, Heidelberg (1973)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T05:01:48Z","timestamp":1706590908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/11538363_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}