{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:17Z","timestamp":1725484637126},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_9","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"115-129","source":"Crossref","is-referenced-by-count":2,"title":["Actual Arithmetic and Feasibility"],"prefix":"10.1007","author":[{"given":"Jean-Yves","family":"Marion","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"A. Asperti. Light affine logic. In Thirteenth Annual IEEE Symposium on Logic in Computer Science(LICS\u201998), pages 300\u2013308, 1998.","DOI":"10.1109\/LICS.1998.705666"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01201998","volume":"2","author":"S. Bellantoni","year":"1992","unstructured":"S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97\u2013110, 1992.","journal-title":"Computational Complexity"},{"key":"9_CR3","unstructured":"S. Bellantoni and M. Hofmann. A new \u201dfeasible\u201d arithmetic. Journal of symbolic logic, 2000. to appear."},{"key":"9_CR4","unstructured":"R. Benzinger. Automated complexity analysis of NUPRL extracts. PhD thesis, Cornell University, 1999."},{"key":"9_CR5","unstructured":"S. Buss. Bounded arithmetic. Bibliopolis, 1986."},{"key":"9_CR6","first-page":"249","volume-title":"Foundations of Secure Computation","author":"N. \u00c7a\u011fman","year":"2000","unstructured":"N. \u00c7a\u011fman, G. Ostrin, and S. Wainer. Proof theoretic complexity of low subrecursive classes. In F. L. Bauer and R. Steinbrueggen, editors, Foundations of Secure Computation, Foundations of Secure Computation, pages 249\u2013286. IOS Press Amsterdam, 2000."},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J-P Jouannaud. Handbook of Theoretical Computer Science vol. B, chapter Rewrite systems, pages 243\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","first-page":"175","volume-title":"Information and Computation","author":"J.-Y. Girard","year":"1998","unstructured":"J.-Y. Girard. Light linear logic. Information and Computation, 143(2):175\u2013204, 1998. pr\u00e9sent\u00e9 \u00e0 LCC\u201994, LNCS 960."},{"key":"9_CR9","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge university press, 1989."},{"key":"9_CR10","unstructured":"A. Heyting. Die formalen regeln der intuitionischen logik. Sitzungsberichte der preussischen akademie von wissenschaften, pages 57\u201371, 1930."},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"P. Scott","year":"1992","unstructured":"P. Scott J.-Y. Girard, A. Scedrov. A modular approach to polynomial-time computability. Theoretical Computer Science, 97(1):1\u201366, 1992.","journal-title":"Theoretical Computer Science"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(98)00357-0","volume":"228","author":"N. Jones","year":"1999","unstructured":"N. Jones. LOGSPACE and PTIME characterized by programming languages. Theoretical Computer Science, 228:151\u2013174, 1999.","journal-title":"Theoretical Computer Science"},{"key":"9_CR13","unstructured":"J.-L. Krivine. Lambda-calcul. Masson, 1990. English translation by R. Cori: Lambda-Calculus, Types and Models (Ellis Horwood Series) 1993."},{"key":"9_CR14","unstructured":"J.L. Krivine and M. Parigot. Programming with proofs. In SCT\u201987, pages 145\u2013159, 1987."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"D. Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In Twenty Fourth Symposium on Foundations of Computer Science, pages 460\u2013469, 1983.","DOI":"10.1109\/SFCS.1983.50"},{"key":"9_CR16","first-page":"279","volume-title":"Logic and Computer Science","author":"D. Leivant","year":"1990","unstructured":"D. Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science, pages 279\u2013327. Academic Press, London, 1990."},{"key":"9_CR17","unstructured":"D. Leivant. A foundational delineation of computational feasiblity. In Proceedings of the Sixth IEEE Symposium on Logic in Computer Science (LICS\u201991), 1991."},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","first-page":"177","volume-title":"Logical and Computational Complexity","author":"D. Leivant","year":"1994","unstructured":"D. Leivant. Intrinsic theories and computational complexity. In Logical and Computational Complexity, volume 960 of Lecture Notes in Computer Science, pages 177\u2013194. Springer, 1994."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"D. Leivant. Predicative recurrence and computational complexity I: Word recurrence and poly-time. In Peter Clote and Jeffery Remmel, editors, Feasible Mathematics II, pages 320\u2013343. Birkh\u00e4user, 1994.","DOI":"10.1007\/978-1-4612-2566-9_11"},{"key":"9_CR20","unstructured":"D. Leivant. Intrinsic reasoning about functional programs I: first order theories. Annals of Pure and Applied Logic, 2000. to appear."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"D. Leivant. Termination proofs and complexity certification. In Proceedings of the third international workshop on Implicit Computational Complexity, 2001.","DOI":"10.1007\/3-540-45500-0_9"},{"key":"9_CR22","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"M. Parigot. Recursive programming with proofs. Theoretical Computer Science, 94:335\u2013356, 1992.","journal-title":"Theoretical Computer Science"},{"key":"9_CR24","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction. Almqvist and Wiskel, Uppsala, 1965."},{"key":"9_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/3-540-48168-0_33","volume-title":"Computer Science Logic, 13th International Workshop, CSL\u2019 99","author":"L. Roversi","year":"1999","unstructured":"L. Roversi. A P-Time completeness proof for light logics. In Computer Science Logic, 13th International Workshop, CSL\u2019 99, volume 1683 of Lecture Notes in Computer Science, pages 469\u2013483, 1999."},{"key":"9_CR26","unstructured":"H. Schwichtenberg. Feasible programs from proofs. http:\/\/www.mathematik.unimuenchen.de\/~schwicht\/ ."},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/BF01620765","volume":"27","author":"H. Simmons","year":"1988","unstructured":"H. Simmons. The realm of primitive recursion. Archive for Mathematical Logic, 27:177\u2013188, 1988.","journal-title":"Archive for Mathematical Logic"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"H. Weyl. \u00fcber die neue grundlagenkrise der mathematik. Mathematische zeitschrift, 1921.","DOI":"10.1007\/BF02102305"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T16:24:32Z","timestamp":1587572672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}