{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:34:08Z","timestamp":1725838448442},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_15","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"203-218","source":"Crossref","is-referenced-by-count":5,"title":["Implicit Computational Complexity of Subrecursive Definitions and Applications to\u00a0Cryptographic Proofs"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Baillot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo Dal","family":"Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Baillot, P., Barthe, G., Dal Lago, U.: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (long version). Technical report, september 2015, HAL archive. http:\/\/hal.archives-ouvertes.fr\/hal-01197456","DOI":"10.1007\/978-3-662-48899-7_15"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.ic.2008.08.005","volume":"207","author":"P Baillot","year":"2009","unstructured":"Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 207(1), 41\u201362 (2009)","journal-title":"Inf. Comput."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: Computer and Communications Securitym, CCS 2010, pp. 375\u2013386. ACM, New York (2010)","DOI":"10.1145\/1866307.1866350"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: Computer and Communications Security, pp. 62\u201373 (1993)","DOI":"10.1145\/168588.168596"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140\u2013154 (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Dal Lago, U.: The geometry of linear higher-order recursion. ACM Trans. Comput. Log. 10(2), 8:1\u20138:38 (2009)","DOI":"10.1145\/1462179.1462180"},{"issue":"4","key":"15_CR10","first-page":"133","volume":"8","author":"U Dal Lago","year":"2011","unstructured":"Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Logical Methods Comput. Sci. 8(4), 133\u2013142 (2011)","journal-title":"Logical Methods Comput. Sci."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Petit, B.: The geometry of types. In: POPL, pp. 167\u2013178 (2013)","DOI":"10.1145\/2480359.2429090"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: POPL, pp. 133\u2013144 (2008)","DOI":"10.1145\/1328897.1328457"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-70936-7_10","volume-title":"Theory of Cryptography","author":"O Goldreich","year":"2007","unstructured":"Goldreich, O.: On expected probabilistic polynomial-time adversaries: a suggestion for restricted definitions and their benefits. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 174\u2013193. Springer, Heidelberg (2007)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Grobauer, B.: Cost recurrences for DML programs. In: International Conference on Functional Programming (ICFP 2001), pp. 253\u2013264 (2001)","DOI":"10.1145\/507669.507666"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127\u2013139 (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"J Hoffmann","year":"2010","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"issue":"1\u20133","key":"15_CR17","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. Ann. Pure Appl. Logic 104(1\u20133), 113\u2013166 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Kristiansen, L.: A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4), 28:1\u201328:41 (2009)","DOI":"10.1145\/1555746.1555752"},{"key":"15_CR19","series-title":"Chapman & Hall Cryptography and Network Security Series","doi-asserted-by":"crossref","DOI":"10.1201\/9781420010756","volume-title":"Introduction to Modern Cryptography","author":"J Katz","year":"2007","unstructured":"Katz, J., Lindell, Y.: Introduction to Modern Cryptography. Chapman & Hall Cryptography and Network Security Series. Chapman & Hall, New York (2007)"},{"issue":"1\/2","key":"15_CR20","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/FI-1993-191-207","volume":"19","author":"D Leivant","year":"1993","unstructured":"Leivant, D., Marion, J.: Lambda calculus characterizations of poly-time. Fundam. Inform. 19(1\/2), 167\u2013184 (1993)","journal-title":"Fundam. Inform."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework (2015). to appear","DOI":"10.1007\/978-3-662-46666-7_4"},{"issue":"1","key":"15_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. High. Order Symb. Comput. 15(1), 91\u2013131 (2002)","journal-title":"High. Order Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,26]],"date-time":"2022-05-26T19:24:02Z","timestamp":1653593042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}