{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:36:13Z","timestamp":1781238973682,"version":"3.54.1"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>We verify the partial correctness of a \"local generic solver\", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for \"spying\", a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley's modulus function, an archetypical example of spying.<\/jats:p>","DOI":"10.1145\/3371101","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Spy game: verifying a local generic solver in Iris"],"prefix":"10.1145","volume":"4","author":[{"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"CNRS, France \/ LRI, France \/ University of Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Martin Abadi and Leslie Lamport. 1988. The Existence of Refinement Mappings. In Logic in Computer Science (LICS). 165\u2013175. https:\/\/www.microsoft.com\/en- us\/research\/publication\/the- existence- of- refinement- mappings\/  Martin Abadi and Leslie Lamport. 1988. The Existence of Refinement Mappings. In Logic in Computer Science (LICS). 165\u2013175. https:\/\/www.microsoft.com\/en- us\/research\/publication\/the- existence- of- refinement- mappings\/"},{"key":"e_1_2_2_2_1","volume-title":"Semantics, Logics, and Calculi \u2013 Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays (Lecture Notes in Computer Science)","author":"Apinis Kalmer","year":"2015"},{"key":"e_1_2_2_3_1","volume-title":"Foundations of Software Science and Computation Structures (FOSSACS) (Lecture Notes in Computer Science)","author":"Bauer Andrej"},{"key":"e_1_2_2_4_1","volume-title":"Foundations of Security Analysis and Design (Lecture Notes in Computer Science)","author":"Besson Fr\u00e9d\u00e9ric"},{"key":"e_1_2_2_5_1","volume-title":"Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science)","author":"Cachera David"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_15"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages (POPL). 238\u2013252. http:\/\/www.di.ens. fr\/~cousot\/publications.www\/CousotCousot- POPL- 77- ACM- p238- - 252- 1977.pdf  Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages (POPL). 238\u2013252. http:\/\/www.di.ens. fr\/~cousot\/publications.www\/CousotCousot- POPL- 77- ACM- p238- - 252- 1977.pdf","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_9_1","unstructured":"Paulo Em\u00edlio de Vilhena Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2020. Coq proofs for \u201cSpy game\u201d. https:\/\/gitlab.inria. fr\/pdevilhe\/spy- game .  Paulo Em\u00edlio de Vilhena Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2020. Coq proofs for \u201cSpy game\u201d. https:\/\/gitlab.inria. fr\/pdevilhe\/spy- game ."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00009-X"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_2_2_13_1","volume-title":"Oracle Semantics for Concurrent Separation Logic. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science)","volume":"4960","author":"Hobor Aquinas","year":"2008"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_21"},{"key":"e_1_2_2_15_1","volume-title":"International Colloquium on Automata, Languages and Programming (Lecture Notes in Computer Science)","author":"Hofmann Martin"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321938"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317775"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Magnus Madsen Ming-Ho Yee and Ondrej Lhot\u00e1k. 2016. From Datalog to Flix: a declarative language for fixed points on lattices. In Programming Language Design and Implementation (PLDI). 194\u2013208. https:\/\/plg.uwaterloo.ca\/~olhotak\/pubs\/ pldi16.pdf  Magnus Madsen Ming-Ho Yee and Ondrej Lhot\u00e1k. 2016. From Datalog to Flix: a declarative language for fixed points on lattices. In Programming Language Design and Implementation (PLDI). 194\u2013208. https:\/\/plg.uwaterloo.ca\/~olhotak\/pubs\/ pldi16.pdf","DOI":"10.1145\/2980983.2908096"},{"key":"e_1_2_2_25_1","volume-title":"Technical Report ACT-DC-153-90. Microelectronics and Computer Technology Corporation","author":"Muthukumar K.","year":"1990"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.024"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.064"},{"key":"e_1_2_2_29_1","unstructured":"Fran\u00e7ois Pottier. 2009. Lazy Least Fixed Points in ML. (2009). http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier- fix.pdf Unpublished.  Fran\u00e7ois Pottier. 2009. Lazy Least Fixed Points in ML. (2009). http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier- fix.pdf Unpublished."},{"key":"e_1_2_2_30_1","unstructured":"Fran\u00e7ois Pottier. 2019. Fix. https:\/\/gitlab.inria.fr\/fpottier\/fix .  Fran\u00e7ois Pottier. 2019. Fix. https:\/\/gitlab.inria.fr\/fpottier\/fix ."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236967"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17548-0"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58485-4_49"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371101","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371101","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":29,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371101"],"URL":"https:\/\/doi.org\/10.1145\/3371101","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}