{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305942,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC","award":["JEP\/N028759\/1"],"award-info":[{"award-number":["JEP\/N028759\/1"]}]},{"name":"Marie Sklodowska--Curie action ``Walgo', program H2020-MSCA-IF-2014","award":["655222"],"award-info":[{"award-number":["655222"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167097","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"146-157","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal proof of polynomial-time complexity with quasi-interpretations"],"prefix":"10.1145","author":[{"given":"Hugo","family":"F\u00e9r\u00e9e","sequence":"first","affiliation":[{"name":"University of Kent, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel","family":"Hym","sequence":"additional","affiliation":[{"name":"University of Lille, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[{"name":"University of Paris 13, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Yves","family":"Moyen","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[{"name":"CNRS, France \/ University of Lille, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings (Lecture Notes in Computer Science), Willy Susilo, Joseph K. Liu, and Yi Mu (Eds.)","volume":"4784","author":"Affeldt Reynald","year":"2007","unstructured":"Reynald Affeldt , Miki Tanaka , and Nicolas Marti . 2007 . Formal Proof of Provable Security by Game-Playing in a Proof Assistant. In Provable Security , First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings (Lecture Notes in Computer Science), Willy Susilo, Joseph K. Liu, and Yi Mu (Eds.) , Vol. 4784 . Springer, 151\u2013168. Reynald Affeldt, Miki Tanaka, and Nicolas Marti. 2007. Formal Proof of Provable Security by Game-Playing in a Proof Assistant. In Provable Security, First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings (Lecture Notes in Computer Science), Willy Susilo, Joseph K. Liu, and Yi Mu (Eds.), Vol. 4784. Springer, 151\u2013168."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_15"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000685"},{"key":"e_1_3_2_1_5_1","volume-title":"Benjamin Gr\u00e9goire, C\u00e9sar Kunz, and Santiago Zanella B\u00e9guelin.","author":"Barthe Gilles","year":"2012","unstructured":"Gilles Barthe , Juan Manuel Crespo , Benjamin Gr\u00e9goire, C\u00e9sar Kunz, and Santiago Zanella B\u00e9guelin. 2012 . Computer-Aided Cryptographic Proofs. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Lecture Notes in Computer Science), Lennart Beringer and Amy P. Felty (Eds.), Vol. 7406 . Springer , 11\u201327. Gilles Barthe, Juan Manuel Crespo, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, and Santiago Zanella B\u00e9guelin. 2012. Computer-Aided Cryptographic Proofs. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Lecture Notes in Computer Science), Lennart Beringer and Amy P. Felty (Eds.), Vol. 7406. Springer, 11\u201327."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_7_1","volume-title":"RSA Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings (Lecture Notes in Computer Science), Aggelos Kiayias (Ed.)","volume":"6558","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , Yassine Lakhnech , and Santiago Zanella B\u00e9guelin . 2011 . Beyond Provable Security Verifiable IND-CCA Security of OAEP. In Topics in Cryptology - CT-RSA 2011 - The Cryptographers\u2019 Track at the RSA Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings (Lecture Notes in Computer Science), Aggelos Kiayias (Ed.) , Vol. 6558 . Springer, 180\u2013196. Gilles Barthe, Benjamin Gr\u00e9goire, Yassine Lakhnech, and Santiago Zanella B\u00e9guelin. 2011. Beyond Provable Security Verifiable IND-CCA Security of OAEP. In Topics in Cryptology - CT-RSA 2011 - The Cryptographers\u2019 Track at the RSA Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings (Lecture Notes in Computer Science), Aggelos Kiayias (Ed.), Vol. 6558. Springer, 180\u2013196."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201998"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.007"},{"key":"e_1_3_2_1_10_1","volume-title":"Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), Yehoshua Bar-Hillel (Ed.). North-Holland Publishing, 24\u201330","author":"Cobham Alan","year":"1965","unstructured":"Alan Cobham . 1965 . The Intrinsic Computational Difficulty of Functions. In Logic , Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), Yehoshua Bar-Hillel (Ed.). North-Holland Publishing, 24\u201330 . Alan Cobham. 1965. The Intrinsic Computational Difficulty of Functions. In Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), Yehoshua Bar-Hillel (Ed.). North-Holland Publishing, 24\u201330."},{"key":"e_1_3_2_1_11_1","first-page":"98","article-title":"The Logic in Computer Science Column Functions versus Algorithms","volume":"65","author":"Colson Lo\u00efc","year":"1998","unstructured":"Lo\u00efc Colson . 1998 . The Logic in Computer Science Column Functions versus Algorithms . Bulletin of the EATCS 65 (1998), 98 \u2013 117 . Lo\u00efc Colson. 1998. The Logic in Computer Science Column Functions versus Algorithms. Bulletin of the EATCS 65 (1998), 98\u2013117.","journal-title":"Bulletin of the EATCS"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9186-x"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.09.006"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_3_2_1_15_1","volume-title":"A detailed proof of the P-criterion. (Oct","author":"F\u00e9r\u00e9e Hugo","year":"2017","unstructured":"Hugo F\u00e9r\u00e9e , Samuel Hym , Micaela Mayero , Jean-Yves Moyen , and David Nowak . 2017. A detailed proof of the P-criterion. (Oct . 2017 ). http:\/\/www.cristal.univ-lille.fr\/~nowakd\/cecoa\/ Hugo F\u00e9r\u00e9e, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. 2017. A detailed proof of the P-criterion. (Oct. 2017). http:\/\/www.cristal.univ-lille.fr\/~nowakd\/cecoa\/"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"volume-title":"The Foundations of Cryptography -","author":"Goldreich Oded","key":"e_1_3_2_1_17_1","unstructured":"Oded Goldreich . 2001. The Foundations of Cryptography - Volume 1 , Basic Techniques. Cambridge University Press . Oded Goldreich. 2001. The Foundations of Cryptography - Volume 1, Basic Techniques. Cambridge University Press."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033952"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90289-R"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00010-5"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.06.008"},{"volume-title":"Introduction to Modern Cryptography","author":"Katz Jonathan","key":"e_1_3_2_1_23_1","unstructured":"Jonathan Katz and Yehuda Lindell . 2014. Introduction to Modern Cryptography , Second Edition. CRC Press . Jonathan Katz and Yehuda Lindell. 2014. Introduction to Modern Cryptography, Second Edition. CRC Press."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00011-7"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.044"},{"key":"e_1_3_2_1_26_1","unstructured":"J.-Y. Moyen and J. G. Simonsen. 2016. More intensional versions of Rice\u2019s Theorem. In Developments in Implicit Computational Complexity DICE\u201916 D. Mazza (Ed.). Eindhoven Netherlands.  J.-Y. Moyen and J. G. Simonsen. 2016. More intensional versions of Rice\u2019s Theorem. In Developments in Implicit Computational Complexity DICE\u201916 D. Mazza (Ed.). Eindhoven Netherlands."},{"key":"e_1_3_2_1_27_1","volume-title":"9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings (Lecture Notes in Computer Science), Sihan Qing, Hideki Imai, and Guilin Wang (Eds.)","volume":"4861","author":"Nowak David","year":"2007","unstructured":"David Nowak . 2007 . A Framework for Game-Based Security Proofs. In Information and Communications Security , 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings (Lecture Notes in Computer Science), Sihan Qing, Hideki Imai, and Guilin Wang (Eds.) , Vol. 4861 . Springer, 319\u2013333. David Nowak. 2007. A Framework for Game-Based Security Proofs. In Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings (Lecture Notes in Computer Science), Sihan Qing, Hideki Imai, and Guilin Wang (Eds.), Vol. 4861. Springer, 319\u2013333."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00730-9_23"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.10.008"},{"key":"e_1_3_2_1_30_1","volume-title":"Subrecursion: Functions and Hierarchies","author":"Rose H. E.","year":"1984","unstructured":"H. E. Rose . 1984 . Subrecursion: Functions and Hierarchies . Oxford University Press . H. E. Rose. 1984. Subrecursion: Functions and Hierarchies. Oxford University Press."},{"key":"e_1_3_2_1_31_1","volume-title":"Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015","author":"Waldmann Johannes","year":"2015","unstructured":"Johannes Waldmann . 2015 . Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015 , June 29 to July 1, 2015, Warsaw, Poland (LIPIcs), Maribel Fern\u00e1ndez (Ed.), Vol. 36. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 318\u2013333. Johannes Waldmann. 2015. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland (LIPIcs), Maribel Fern\u00e1ndez (Ed.), Vol. 36. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 318\u2013333."},{"key":"e_1_3_2_1_32_1","volume-title":"Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1","author":"Zankl Harald","year":"2014","unstructured":"Harald Zankl and Martin Korp . 2014. Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1 ( 2014 ). Harald Zankl and Martin Korp. 2014. Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1 (2014)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000265"}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167097","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167097","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167097"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":33,"alternative-id":["10.1145\/3167097","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167097","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}