{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:59:19Z","timestamp":1767920359334,"version":"3.49.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2311983"],"award-info":[{"award-number":["2311983"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2525102"],"award-info":[{"award-number":["2525102"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-0009"],"award-info":[{"award-number":["FA9550-21-0009"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-23-1-0434"],"award-info":[{"award-number":["FA9550-23-1-0434"]}],"id":[{"id":"10.13039\/100000181","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":[[2026,1,8]]},"abstract":"<jats:p>As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step semantics, which must dwell on every intermediate program state, big-step semantics conveniently jumps directly to the ever-important result of the computation. Big-step semantics also typically involves fewer inference rules than their small-step counterparts. However, in exchange for ergonomics, big-step semantics gives up power: Small-step semantics describes program behaviors that are outside the grasp of big-step semantics, notably divergence.<\/jats:p>\n                  <jats:p>This work presents a little-known extension of big-step semantics with inductive definitions that captures diverging computations without introducing error states. This big-stop semantics is illustrated for typed, untyped, and effectful variants of PCF. Big-stop semantics extends the standard big-step inference rules with a few additional rules to define an evaluation judgment that is equivalent to the reflexive-transitive closure of small-step transitions. This simple extension contrasts with other solutions in the literature that sacrifice ergonomics by introducing many additional inference rules, global state, and\/or less-commonly-understood reasoning principles like coinduction. The ergonomics of big-stop semantics is exemplified via concise Agda proofs for some key results and compilation theorems.<\/jats:p>","DOI":"10.1145\/3776718","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2204-2232","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4595-7088","authenticated-orcid":false,"given":"David M.","family":"Kahn","sequence":"first","affiliation":[{"name":"Denison University, Granville, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8326-0788","authenticated-orcid":false,"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7600-9069","authenticated-orcid":false,"given":"Runming","family":"Li","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2022. WebAssembly Core Specification. https:\/\/www.w3.org\/TR\/wasm-core-2\/"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"102492","DOI":"10.1016\/j.scico.2020.102492","article-title":"A big step from finite to infinite computations","volume":"197","author":"Ancona Davide","year":"2020","unstructured":"Davide Ancona, Francesco Dagnino, Jurriaan Rot, and Elena Zucca. 2020. A big step from finite to infinite computations. Science of Computer Programming, 197 (2020), 102492.","journal-title":"Science of Computer Programming"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-009-9148-3"},{"key":"e_1_2_1_5_1","volume-title":"General recursion via coinductive types. Logical Methods in Computer Science, 1","author":"Capretta Venanzio","year":"2005","unstructured":"Venanzio Capretta. 2005. General recursion via coinductive types. Logical Methods in Computer Science, 1 (2005)."},{"key":"e_1_2_1_6_1","volume-title":"European Symposium on Programming. 41\u201360","author":"Chargu\u00e9raud Arthur","year":"2013","unstructured":"Arthur Chargu\u00e9raud. 2013. Pretty-big-step semantics. In European Symposium on Programming. 41\u201360."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143184"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.03.025"},{"key":"e_1_2_1_9_1","unstructured":"Roy L Crole. 1998. Lectures on [Co] induction and [Co] algebras. Technical Report 1998\/12 Department of Mathematics and Computer Science \u2026."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3522729"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364546"},{"key":"e_1_2_1_12_1","volume-title":"The next 700 Krivine machines. Higher-order and symbolic computation, 20","author":"Douence R\u00e9mi","year":"2007","unstructured":"R\u00e9mi Douence and Pascal Fradet. 2007. The next 700 Krivine machines. Higher-order and symbolic computation, 20 (2007), 237\u2013255."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111062"},{"key":"e_1_2_1_15_1","volume-title":"The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph. D. Dissertation","author":"Felleisen Matthias","unstructured":"Matthias Felleisen. 1987. The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph. D. Dissertation. Indiana University."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/173262.155113"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Maurizio Gabbrielli and Simone Martini. 2010. Abstract Machines. Springer London London. 1\u201325. isbn:978-1-84882-914-5 https:\/\/doi.org\/10.1007\/978-1-84882-914-5_1 10.1007\/978-1-84882-914-5_1","DOI":"10.1007\/978-1-84882-914-5_1"},{"key":"e_1_2_1_18_1","unstructured":"Carl A Gunter and Didier R\u00e9my. 1993. A proof-theoretic assessment of runtime type errors. In Technical Report 11261921230-43TM. Citeseer."},{"key":"e_1_2_1_19_1","volume-title":"Practical foundations for programming languages","author":"Harper Robert","unstructured":"Robert Harper. 2016. Practical foundations for programming languages. Cambridge University Press."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_2_1_21_1","volume-title":"Asian Symposium on Programming Languages and Systems. 172\u2013187","author":"Hoffmann Jan","year":"2010","unstructured":"Jan Hoffmann and Martin Hofmann. 2010. Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In Asian Symposium on Programming Languages and Systems. 172\u2013187."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604148"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224191"},{"key":"e_1_2_1_25_1","unstructured":"Neil D Jones Carsten K Gomard and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Peter Sestoft."},{"key":"e_1_2_1_26_1","volume-title":"Leveraging Linearity to Improve Automatic Amortized Resource Analysis. Ph. D. Dissertation","author":"Kahn David","unstructured":"David Kahn. 2024. Leveraging Linearity to Improve Automatic Amortized Resource Analysis. Ph. D. Dissertation. Carnegie Mellon University."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"David Kahn Jan Hoffmann and Runming Li. 2025. Big-Stop Semantics. https:\/\/doi.org\/10.5281\/zenodo.17316781 10.5281\/zenodo.17316781","DOI":"10.5281\/zenodo.17316781"},{"key":"e_1_2_1_28_1","unstructured":"David M Kahn Jan Hoffmann and Runming Li. 2025. Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment. arxiv:2508.15157. arxiv:2508.15157"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039592"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_2_1_31_1","volume-title":"A call-by-name lambda-calculus machine. Higher-order and symbolic computation, 20","author":"Krivine Jean-Louis","year":"2007","unstructured":"Jean-Louis Krivine. 2007. A call-by-name lambda-calculus machine. Higher-order and symbolic computation, 20 (2007), 199\u2013207."},{"key":"e_1_2_1_32_1","volume-title":"The mechanical evaluation of expressions. The computer journal, 6, 4","author":"Landin Peter J","year":"1964","unstructured":"Peter J Landin. 1964. The mechanical evaluation of expressions. The computer journal, 6, 4 (1964), 308\u2013320."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_34_1","unstructured":"Xavier Leroy. 1990. The ZINC experiment: an economical implementation of the ML language. Ph. D. Dissertation. INRIA."},{"key":"e_1_2_1_35_1","volume-title":"Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 42\u201354","author":"Leroy Xavier","year":"2006","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 42\u201354."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_2_1_37_1","volume-title":"Definition of standard ML","author":"Milner Robin","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. 1990. Definition of standard ML. MIT Press. isbn:978-0-262-63132-7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_26"},{"key":"e_1_2_1_39_1","volume-title":"C formalised in HOL. Ph. D. Dissertation","author":"Norrish Michael","unstructured":"Michael Norrish. 1999. C formalised in HOL. Ph. D. Dissertation. University of Cambridge, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.624131"},{"key":"e_1_2_1_40_1","volume-title":"LCF considered as a programming language. Theoretical computer science, 5, 3","author":"Plotkin Gordon D.","year":"1977","unstructured":"Gordon D. Plotkin. 1977. LCF considered as a programming language. Theoretical computer science, 5, 3 (1977), 223\u2013255."},{"key":"e_1_2_1_41_1","unstructured":"Gordon D Plotkin. 1981. A structural approach to operational semantics."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1016\/j.jlamp.2016.05.001","article-title":"Flag-based big-step semantics","volume":"88","author":"Poulsen Casper Bach","year":"2017","unstructured":"Casper Bach Poulsen and Peter D Mosses. 2017. Flag-based big-step semantics. Journal of Logical and Algebraic Methods in Programming, 88 (2017), 174\u2013190.","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Amr Sabry and Matthias Felleisen. 1992. Reasoning about programs in continuation-passing style.. ACM SIGPLAN Lisp Pointers 288\u2013298.","DOI":"10.1145\/141478.141563"},{"key":"e_1_2_1_44_1","unstructured":"Jeremy Siek. 2012. Big-step diverging or stuck? https:\/\/siek.blogspot.com\/2012\/07\/big-step-diverging-or-stuck.html"},{"key":"e_1_2_1_45_1","unstructured":"Martin Strecker. 2005. Compiler verification for C0 (intermediate report). Tech. rep. Universit\u00e9 Paul Sabatier Toulouse."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_2_1_47_1","volume-title":"A syntactic approach to type soundness. Information and computation, 115, 1","author":"Wright Andrew K","year":"1994","unstructured":"Andrew K Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation, 115, 1 (1994), 38\u201394."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.3390\/math10203800"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776718","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:30Z","timestamp":1767899010000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776718"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776718"],"URL":"https:\/\/doi.org\/10.1145\/3776718","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}