{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:11:00Z","timestamp":1775671860745,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521584"],"award-info":[{"award-number":["1521584"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE2140739"],"award-info":[{"award-number":["DGE2140739"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779088","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"187-200","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Foundational Verification of Running-Time Bounds for Interactive Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-8749-4332","authenticated-orcid":false,"given":"Andy","family":"Tockman","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Boston, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7139-2334","authenticated-orcid":false,"given":"Pratap","family":"Singh","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Google, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Boston, USA"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_2_1_3_1","volume-title":"Tech. Rep. UCB\/EECS-2016-17, 4","author":"Asanovic Krste","year":"2016","unstructured":"Krste Asanovic, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, et al. 2016. The Rocket Chip generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17, 4 (2016), 6\u20132."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_3"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729249"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74130-5_14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951950"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729318"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656446"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544885.3544887"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428272"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656439"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486169"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_1_20_1","volume-title":"Amortized Resource Analysis with Polynomial Potential","author":"Hoffmann Jan","year":"1957","unstructured":"Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In Programming Languages and Systems, Andrew D. Gordon (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 287\u2013306. isbn:978-3-642-11957-6"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.WCET.2014.11"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68671-1_5"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341687"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"A. Pnueli M. Siegel and E. Singerman. 1998. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems Bernhard Steffen (Ed.). Springer Berlin Heidelberg Berlin Heidelberg. 151\u2013166. isbn:978-3-540-69753-4","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779088","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:53:51Z","timestamp":1775667231000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":31,"alternative-id":["10.1145\/3779031.3779088","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779088","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}