{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:17Z","timestamp":1740123377746,"version":"3.37.3"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T00:00:00Z","timestamp":1564531200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T00:00:00Z","timestamp":1564531200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10817-019-09530-2","type":"journal-article","created":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T09:02:50Z","timestamp":1564563770000},"page":"813-855","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs"],"prefix":"10.1007","volume":"63","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,31]]},"reference":[{"key":"9530_CR1","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci. 12(1) (2016)","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"9530_CR2","doi-asserted-by":"crossref","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: Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, pp. 113\u2013132 (2007)","DOI":"10.1007\/978-3-540-92188-2_5"},{"key":"9530_CR3","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-662-48899-7_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Patrick Baillot","year":"2015","unstructured":"Baillot, P., Barthe, G., Dal Lago, U.: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. In: Proceedings of LPAR 2015, Volume 9450 of LNCS, pp. 203\u2013218. Springer, Berlin (2015)"},{"issue":"1","key":"9530_CR4","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":"9530_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: Proceedings of Computer and Communications Security, CCS 2010, pp. 375\u2013386. ACM, New York (2010)","DOI":"10.1145\/1866307.1866350"},{"key":"9530_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P.-Y., Swamy, N., Zanella-B\u00e9guelin, S.: Probabilistic relational verification for cryptographic implementations. In: Proceedings of POPL 2014, pp. 193\u2013206 (2014)","DOI":"10.1145\/2578855.2535847"},{"issue":"1","key":"9530_CR7","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/2775051.2677000","volume":"50","author":"Gilles Barthe","year":"2015","unstructured":"Barthe, G., Gaboardi, M., Gallego\u00a0Arias, E.\u00a0J., Hsu, J., Roth, A., Strub, P.-Y.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: Proceedings of POPL 2015, pp. 55\u201368. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"9530_CR8","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/1594834.1480894","volume":"44","author":"Gilles Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Proceedings of POPL 2009, pp. 90\u2013101 (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"9530_CR9","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":"Gilles Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Proceedings of CRYPTO 2011, pp. 71\u201390 (2011)"},{"key":"9530_CR10","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: Proceedings of Computer and Communications Security, pp. 62\u201373 (1993)","DOI":"10.1145\/168588.168596"},{"key":"9530_CR11","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"},{"issue":"2","key":"9530_CR12","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1462179.1462180","volume":"10","author":"U Dal Lago","year":"2009","unstructured":"Dal Lago, U.: The geometry of linear higher-order recursion. ACM Trans. Comput. Log. 10(2), 8:1\u20138:38 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"9530_CR13","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Log. Methods Comput. Sci. 8(4) (2011)","DOI":"10.2168\/LMCS-8(4:11)2012"},{"issue":"1","key":"9530_CR14","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/2480359.2429090","volume":"48","author":"Ugo Dal lago","year":"2013","unstructured":"Dal Lago, U., Petit, B.: The geometry of types. In: Proceedings of POPL 2013, pp. 167\u2013178 (2013)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"9530_CR15","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1328897.1328457","volume":"43","author":"Nils Anders Danielsson","year":"2008","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of POPL 2008, pp. 133\u2013144 (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"9530_CR16","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the lambda-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts (1986)"},{"key":"9530_CR17","doi-asserted-by":"crossref","unstructured":"Goldreich, O.: On expected probabilistic polynomial-time adversaries: a suggestion for restricted definitions and their benefits. In: Theory of Cryptography, pp. 174\u2013193. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-70936-7_10"},{"key":"9530_CR18","doi-asserted-by":"crossref","unstructured":"Grobauer, B.: Cost recurrences for DML programs. In: International Conference on Functional Programming (ICFP \u201901), pp. 253\u2013264 (2001)","DOI":"10.1145\/507635.507666"},{"issue":"1","key":"9530_CR19","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/1594834.1480898","volume":"44","author":"Sumit Gulwani","year":"2009","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of POPL 2009, pp. 127\u2013139 (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"9530_CR20","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive, p. 181 (2005)"},{"key":"9530_CR21","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"Jan Hoffmann","year":"2010","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Proceedings of ESOP 2010, pp. 287\u2013306 (2010)"},{"issue":"1\u20133","key":"9530_CR22","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. Log. 104(1\u20133), 113\u2013166 (2000)","journal-title":"Ann. Pure Appl. Log."},{"issue":"4","key":"9530_CR23","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1555746.1555752","volume":"10","author":"ND Jones","year":"2009","unstructured":"Jones, N.D., Kristiansen, L.: A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4), 28 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"9530_CR24","series-title":"Chapman & Hall Cryptography and Network Security Series","doi-asserted-by":"publisher","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, London (2007)"},{"issue":"1\/2","key":"9530_CR25","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.-Y.: Lambda calculus characterizations of poly-time. Fundam. Inform. 19(1\/2), 167\u2013184 (1993)","journal-title":"Fundam. Inform."},{"key":"9530_CR26","unstructured":"Lesourd, M.: Type inference for complexity analysis of functional programs (2016). Master Thesis, ENS Lyon. https:\/\/ilsordo.github.io\/research\/rapport2016.pdf"},{"key":"9530_CR27","first-page":"53","volume-title":"Lecture Notes in Computer Science","author":"Adam Petcher","year":"2015","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Proceedings of POST 2015, Volume 9036 of LNCS, pp. 203\u2013218 (2015)"},{"key":"9530_CR28","doi-asserted-by":"crossref","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Proceedings of ICFP 2011, pp. 266\u2013278 (2011)","DOI":"10.1145\/2034574.2034811"},{"issue":"1","key":"9530_CR29","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. Higher-Order Symb. Comput. 15(1), 91\u2013131 (2002)","journal-title":"Higher-Order Symb. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09530-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09530-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09530-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T22:22:20Z","timestamp":1664058140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09530-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,31]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9530"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09530-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,7,31]]},"assertion":[{"value":"20 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 July 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}