{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:08:01Z","timestamp":1760044081656,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["715753"],"award-info":[{"award-number":["715753"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>\n            We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property\n            <jats:italic>witnessed<\/jats:italic>\n            in a prior state can be soundly\n            <jats:italic>recalled<\/jats:italic>\n            in the current state, provided (1)\u00a0state evolves according to a given preorder, and (2)\u00a0the property is preserved by this preorder. In many scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the\n            <jats:italic>monotonic-state monad<\/jats:italic>\n            , a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F\n            <jats:sup>\u22c6<\/jats:sup>\n            verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.\n          <\/jats:p>","DOI":"10.1145\/3158153","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Recalling a witness: foundations and applications of monotonic state"],"prefix":"10.1145","volume":"2","author":[{"given":"Danel","family":"Ahman","sequence":"first","affiliation":[{"name":"Inria, France"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS Paris, France"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"volume-title":"SNAPL","year":"2017","author":"Bhargavan K.","key":"e_1_2_2_5_1"},{"volume-title":"Implementing and proving the TLS 1.3 record layer","year":"2017","author":"Bhargavan K.","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3051092"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2462156.2462160"},{"volume-title":"A monadic framework for relational verification: Applied to information security, program equivalence, and optimizations . arXiv:1703.00055","year":"2017","author":"Grimm N.","key":"e_1_2_2_14_1"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_22_1","series-title":"Semantics Structures in Computation","volume-title":"A Functional\/Imperative Synthesis","author":"Levy P. B.","year":"2004"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_20"},{"volume-title":"Lectures on the Coupling Method","year":"2002","author":"Lindvall T.","key":"e_1_2_2_24_1"},{"volume-title":"Rote: Rollback protection for trusted execution . USENIX Security","year":"2017","author":"Matetic S.","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/420956"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.38"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480890"},{"volume-title":"A logic for shared mutable data structures . LICS","year":"2002","author":"Reynolds J. C.","key":"e_1_2_2_34_1"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"volume-title":"Ariadne: A minimal approach to state continuity . USENIX Security","year":"2016","author":"Strackx R.","key":"e_1_2_2_36_1"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000142"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158153"],"URL":"https:\/\/doi.org\/10.1145\/3158153","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}