{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:35Z","timestamp":1772498915216,"version":"3.50.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T00:00:00Z","timestamp":1678233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>\n            This article gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions (hence the name\n            <jats:italic>omni<\/jats:italic>\n            ), whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution. This restructuring allows for straightforward modeling of both nondeterminism and undefined behavior as commonly encountered in sequential functional and imperative programs. Specifically, omnisemantics inherently assert\n            <jats:italic>safety<\/jats:italic>\n            (i.e., they guarantee that none of the execution branches gets stuck), while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism.\n          <\/jats:p>\n          <jats:p>Omnisemantics can be understood as an inductively defined weakest-precondition semantics (or more generally, predicate-transformer semantics) that does not involve invariants for loops and recursion but instead uses unrolling rules like in traditional small-step and big-step semantics. Omnisemantics were previously described in association with several projects, but we believe the technique has been underappreciated and deserves a well-motivated, extensive, and pedagogical presentation of its benefits. We also explore several novel aspects associated with these semantics, in particular, their use in type-safety proofs for lambda calculi, partial-correctness reasoning, and forward proofs of compiler correctness for terminating but potentially nondeterministic programs being compiled to nondeterministic target languages. All results in this article are formalized in Coq.<\/jats:p>","DOI":"10.1145\/3579834","type":"journal-article","created":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T12:04:34Z","timestamp":1674561874000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Omnisemantics: Smooth Handling of Nondeterminism"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7764-4507","authenticated-orcid":false,"given":"Arthur","family":"Chargu\u00e9raud","sequence":"first","affiliation":[{"name":"Inria &amp; Universit\u00e9 de Strasbourg, CNRS, ICube, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,3,8]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460860"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009878"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90055-5"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.47"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_3_9_1","unstructured":"Qinxiang Cao Shengyi Wang Aquinas Hobor and Andrew W. Appel. 2018. Proof pearl: Magic wand as frame. Unpublished."},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_3_11_1","first-page":"418","volume-title":"International Conference on Functional Programming (ICFP\u201911)","author":"Chargu\u00e9raud Arthur","year":"2011","unstructured":"Arthur Chargu\u00e9raud. 2011. Characteristic formulae for the verification of imperative programs. In International Conference on Functional Programming (ICFP\u201911). Association for Computing Machinery, 418\u2013430. 10.1145\/2034773.2034828"},{"key":"e_1_3_3_12_1","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-37036-6_3","volume-title":"Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP \u201913)","author":"Chargu\u00e9raud Arthur","year":"2013","unstructured":"Arthur Chargu\u00e9raud. 2013. Pretty-big-step semantics. In Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP \u201913). Springer-Verlag, 41\u201360. 10.1007\/978-3-642-37036-6_3"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_3_3_14_1","first-page":"142","volume-title":"A Modern Eye on Separation Logic for Sequential Programs","author":"Chargu\u00e9raud Arthur","year":"2022","unstructured":"Arthur Chargu\u00e9raud. 2022. A Modern Eye on Separation Logic for Sequential Programs. Technical Report. 142 pages. https:\/\/hal.inria.fr\/hal-03864664v1."},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_3_3_16_1","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/2500365.2500592","volume-title":"Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201913)","author":"Chlipala Adam","year":"2013","unstructured":"Adam Chlipala. 2013. The bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201913). Association for Computing Machinery, 391\u2013402. 10.1145\/2500365.2500592"},{"key":"e_1_3_3_17_1","first-page":"83","volume-title":"Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201992)","author":"Cousot Patrick","year":"1992","unstructured":"Patrick Cousot and Radhia Cousot. 1992. Inductive definitions, semantics and abstract interpretations. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201992). Association for Computing Machinery, 83\u201394. 10.1145\/143165.143184"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364546"},{"key":"e_1_3_3_19_1","volume-title":"A Discipline of Programming.","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming.Prentice-Hall. I\u2013XVII, 1\u2013217 pages."},{"key":"e_1_3_3_20_1","first-page":"604","volume-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201921)","author":"Erbsen Andres","year":"2021","unstructured":"Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. 2021. Integration verification across software and hardware for a simple embedded system. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201921). Association for Computing Machinery, 604\u2013619. 10.1145\/3453483.3454065"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2677001"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90006-0"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"e_1_3_3_24_1","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1145\/2429069.2429131","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201913)","author":"Hobor Aquinas","year":"2013","unstructured":"Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201913). Association for Computing Machinery, 523\u2013536. 10.1145\/2429069.2429131"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_26_1","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1145\/2676726.2676980","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201915)","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201915). Association for Computing Machinery, 637\u2013650. 10.1145\/2676726.2676980"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_3_28_1","first-page":"234","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP\u201919)","author":"Koh Nicolas","year":"2019","unstructured":"Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honor\u00e9, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. From C to interaction trees: Specifying, verifying, and testing a networked server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP\u201919). Association for Computing Machinery, 234\u2013248. 10.1145\/3293880.3294106"},{"key":"e_1_3_3_29_1","volume-title":"The C Standard Formalized in Coq","author":"Krebbers Robbert","year":"2015","unstructured":"Robbert Krebbers. 2015. The C Standard Formalized in Coq. Ph.D. Dissertation. Radboud University Nijmegen. https:\/\/robbertkrebbers.nl\/research\/thesis.pdf."},{"key":"e_1_3_3_30_1","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/1708016.1708025","volume-title":"Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI\u201910)","author":"Krishnaswami Neel R.","year":"2010","unstructured":"Neel R. Krishnaswami, Lars Birkedal, and Jonathan Aldrich. 2010. Verifying event-driven programs using ramified frame properties. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI\u201910). Association for Computing Machinery, 63\u201376. 10.1145\/1708016.1708025"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_3_3_34_1","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","article-title":"Forward and backward simulations part I: Untimed Systems","volume":"121","author":"Lynch Nancy","year":"1995","unstructured":"Nancy Lynch and Frits Vaandrager. 1995. Forward and backward simulations part I: Untimed Systems. Information and Computation 121 (1995), 214\u2013233.","journal-title":"Information and Computation"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_3_36_1","volume-title":"Abstraction, Refinement And Proof For Probabilistic Systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement And Proof For Probabilistic Systems. Springer."},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_3_39_1","first-page":"157","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Milner Robin","year":"1975","unstructured":"Robin Milner. 1975. Processes: A mathematical model of computing agents. In Studies in Logic and the Foundations of Mathematics. Vol. 80. Elsevier, 157\u2013173."},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_25"},{"key":"e_1_3_3_41_1","article-title":"Mixed induction-coinduction at work for Coq","author":"Nakata Keiko","year":"2010","unstructured":"Keiko Nakata and Tarmo Uustalu. 2010. Mixed induction-coinduction at work for Coq. In 2nd Workshop of Coq Users, Developers, and Contributors (2010). http:\/\/www.cs.ioc.ee\/ keiko\/papers\/Coq2.pdf.","journal-title":"2nd Workshop of Coq Users, Developers, and Contributors"},{"key":"e_1_3_3_42_1","first-page":"320","volume-title":"Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201906)","author":"Ni Zhaozhong","year":"2006","unstructured":"Zhaozhong Ni and Zhong Shao. 2006. Certified assembly programming with embedded code pointers. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201906). Association for Computing Machinery, 320\u2013333. 10.1145\/1111037.1111066"},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_3_45_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","year":"2002","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_3_3_46_1","doi-asserted-by":"crossref","DOI":"10.1137\/0205035","article-title":"A powerdomain construction","author":"Plotkin G. D.","year":"1976","unstructured":"G. D. Plotkin. 1976. A powerdomain construction. Siam J. of Computing (1976).","journal-title":"Siam J. of Computing"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_3_48_1","doi-asserted-by":"crossref","first-page":"624","DOI":"10.1145\/2983990.2984008","volume-title":"Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications","author":"Rompf Tiark","year":"2016","unstructured":"Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, 624\u2013641. 10.1145\/2983990.2984008"},{"key":"e_1_3_3_49_1","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/2854065.2854083","volume-title":"Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs","author":"Sch\u00e4fer Steven","year":"2016","unstructured":"Steven Sch\u00e4fer, Sigurd Schneider, and Gert Smolka. 2016. Axiomatic semantics for compiler verification. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM, 188\u2013196. 10.1145\/2854065.2854083"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:4)2013"},{"key":"e_1_3_3_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_3_52_1","first-page":"80","volume-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201921)","author":"Spies Simon","year":"2021","unstructured":"Simon Spies, Lennard G\u00e4her, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2021. Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201921). Association for Computing Machinery, 80\u201395. 10.1145\/3453483.3454031"},{"key":"e_1_3_3_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_28"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_3_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.016"},{"key":"e_1_3_3_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_3_3_58_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_3_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579834","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3579834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:27Z","timestamp":1750182687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579834"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,8]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3579834"],"URL":"https:\/\/doi.org\/10.1145\/3579834","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,8]]},"assertion":[{"value":"2022-03-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-16","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}