{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T10:23:56Z","timestamp":1794392636007,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_11","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"119-134","source":"Crossref","is-referenced-by-count":1,"title":["A Formalization of Polytime Functions"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Heraud","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-78969-7_11","volume-title":"Functional and Logic Programming","author":"M. Avanzini","year":"2008","unstructured":"Avanzini, M., Moser, G.: Complexity Analysis by Rewriting. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 130\u2013146. Springer, Heidelberg (2008)"},{"key":"11_CR2","volume-title":"ACM Transactions on Computational Logic","author":"T. Arai","year":"2009","unstructured":"Arai, T., Eguchi, N.: A new function algebra of EXPTIME functions by safe nested recursion. In: ACM Transactions on Computational Logic, vol.\u00a010(4). ACM, New York (2009)"},{"key":"11_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-89439-1_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Backes","year":"2008","unstructured":"Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 353\u2013376. Springer, Heidelberg (2008)"},{"key":"11_CR4","first-page":"90","volume-title":"Proceedings of the 36th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL 2009)","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: Proceedings of the 36th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL 2009), pp. 90\u2013101. ACM, New York (2009)"},{"key":"11_CR5","unstructured":"Bellantoni, S.: Predicative Recursion and Computational Complexity. PhD Thesis, University of Toronto (1992)"},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01201998","volume":"2","author":"S. Bellantoni","year":"1992","unstructured":"Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity\u00a02, 97\u2013110 (1992)","journal-title":"Computational Complexity"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"M. Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework\u00a0for\u00a0code-based\u00a0game-playing\u00a0proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006)"},{"key":"11_CR8","first-page":"24","volume-title":"Proceedings of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science","author":"A. Cobham","year":"1964","unstructured":"Cobham, A.: The intrinsic computational difficulty of functions. In: Proceedings of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science, pp. 24\u201330. North-Holland, Amsterdam (1964)"},{"issue":"6","key":"11_CR9","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W. Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT\u00a022(6), 644\u2013654 (1976)","journal-title":"IEEE Transactions on Information Theory IT"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving Equalities in a Commutative Ring Done Right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"11_CR11","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005)"},{"issue":"1-3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0168-0072(00)00010-5","volume":"104","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic\u00a0104(1-3), 113\u2013166 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/LICS.1991.151625","volume-title":"Sixth Annual IEEE Symposium on Logic in Computer Science","author":"D. Leivant","year":"1991","unstructured":"Leivant, D.: A foundational delineation of computational feasibility. In: Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 2\u201311. IEEE Computer Society, Los Alamitos (1991)"},{"key":"11_CR14","first-page":"725","volume-title":"Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS 1998)","author":"J.C. Mitchell","year":"1998","unstructured":"Mitchell, J.C., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS 1998), pp. 725\u2013733. IEEE Computer Society, Los Alamitos (1998)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-77048-0_25","volume-title":"Information and Communications Security","author":"D. Nowak","year":"2007","unstructured":"Nowak, D.: A framework for game-based security proofs. In: Qing, S., Imai, H., Wang, G. (eds.) ICICS 2007. LNCS, vol.\u00a04861, pp. 319\u2013333. Springer, Heidelberg (2007)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-16280-0_3","volume-title":"Provable Security","author":"D. Nowak","year":"2010","unstructured":"Nowak, D., Zhang, Y.: A calculus for game-based security proofs. In: Heng, S.-H., Kurosawa, K. (eds.) ProvSec 2010. LNCS, vol.\u00a06402, pp. 35\u201352. Springer, Heidelberg (2010)"},{"key":"11_CR17","volume-title":"Subrecursion: functions and hierarchies. Oxford Logic Guides 9","author":"H.E. Rose","year":"1984","unstructured":"Rose, H.E.: Subrecursion: functions and hierarchies. Oxford Logic Guides 9. Clarendon Press, Oxford (1984)"},{"key":"11_CR18","unstructured":"Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004)"},{"key":"11_CR19","volume-title":"Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding (MERLIN 2003)","author":"C. Sch\u00fcrmann","year":"2003","unstructured":"Sch\u00fcrmann, C., Shah, J.: Representing reductions of NP-complete problems in logical frameworks: A case study. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding (MERLIN 2003). ACM, New York (2003)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/11538363_36","volume-title":"Computer Science Logic","author":"C. Sch\u00fcrmann","year":"2005","unstructured":"Sch\u00fcrmann, C., Shah, J.: Identifying Polynomial-Time Recursive Functions. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 525\u2013540. Springer, Heidelberg (2005)"},{"key":"11_CR21","unstructured":"Tourlakis, G.J.: Computability, Reston (1984)"},{"key":"11_CR22","first-page":"951","volume-title":"Mathematical Structures in Computer Science","author":"Y. Zhang","year":"2010","unstructured":"Zhang, Y.: The computational SLR: a logic for reasoning about computational indistinguishability. In: Mathematical Structures in Computer Science, vol.\u00a020, pp. 951\u2013975. Cambridge University Press, Cambridge (2010)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T02:27:16Z","timestamp":1553999236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_11","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}