{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:44Z","timestamp":1750309184780,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"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":[[2024,4,29]]},"abstract":"<jats:p>\n            This paper develops a novel minimal-state operational semantics for higher-order functional languages that uses\n            <jats:italic>only<\/jats:italic>\n            the call stack and a source program point or a lexical level as the\n            <jats:italic>complete<\/jats:italic>\n            state information: there is no environment, no substitution, no continuation, etc. We prove this form of operational semantics equivalent to standard presentations.\n          <\/jats:p>\n          <jats:p>We then show how this approach can open the door to potential new applications: we define a program analysis as a direct finitization of this operational semantics. The program analysis that naturally emerges has a number of novel and interesting properties compared to standard program analyses for higher-order programs: for example, it can infer recurrences and does not need value widening. We both give a formal definition of the analysis and describe our current implementation.<\/jats:p>","DOI":"10.1145\/3649852","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1154-1180","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Pure Demand Operational Semantics with Applications to Program Analysis"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-0495-2716","authenticated-orcid":false,"given":"Scott","family":"Smith","sequence":"first","affiliation":[{"name":"Johns Hopkins University, Baltimore, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8853-5813","authenticated-orcid":false,"given":"Robert","family":"Zhang","sequence":"additional","affiliation":[{"name":"Johns Hopkins University, Baltimore, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt H.","unstructured":"H. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics (2nd ed.).","edition":"2"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290357"},{"key":"e_1_2_2_3_1","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL \u201977)","author":"Cousot Patrick","year":"1977","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 Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL \u201977). ACM, New York, NY, USA. 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973 10.1145\/512950.512973"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310340"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_1"},{"key":"e_1_2_2_7_1","volume-title":"Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III","author":"Felleisen Matthias","year":"1986","unstructured":"Matthias Felleisen and Daniel P. Friedman. 1987. Control operators, the SECD-machine, and the \u03bb -calculus. In Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, Martin Wirsing (Ed.). North-Holland, 193\u2013222."},{"key":"e_1_2_2_8_1","unstructured":"Charles Fischer. 2005. CS536 Lecture Notes. https:\/\/pages.cs.wisc.edu\/~fischer\/cs536.s05\/course.hold\/html\/NOTES\/8.RUNTIME-VAR-ACCESS.html##accessLink"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143172"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199536"},{"key":"e_1_2_2_13_1","unstructured":"Roshan James. 2014. Core_bench: better micro-benchmarks through linear regression. https:\/\/blog.janestreet.com\/core_bench-micro-benchmarking-for-ocaml"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201914)","author":"Kaki Gowtham","year":"2014","unstructured":"Gowtham Kaki and Suresh Jagannathan. 2014. A Relational Framework for Higher-Order Shape Analysis. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201914). Association for Computing Machinery, New York, NY, USA. 311\u2013324. isbn:9781450328739 https:\/\/doi.org\/10.1145\/2628136.2628159 10.1145\/2628136.2628159"},{"key":"e_1_2_2_15_1","volume-title":"Proc. ACM Program. Lang., 2, ICFP","author":"Koppel James","year":"2018","unstructured":"James Koppel, Gabriel Scherer, and Armando Solar-Lezama. 2018. Capturing the Future by Replaying the Past (Functional Pearl). Proc. ACM Program. Lang., 2, ICFP (2018), Article 76, jul, 29 pages. https:\/\/doi.org\/10.1145\/3236771 10.1145\/3236771"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the 17th International Conference on Static Analysis (SAS\u201910)","author":"Might Matthew","year":"2010","unstructured":"Matthew Might. 2010. Abstract Interpreters for Free. In Proceedings of the 17th International Conference on Static Analysis (SAS\u201910). Springer-Verlag, Berlin, Heidelberg. 407\u2013421. isbn:3-642-15768-8, 978-3-642-15768-4 http:\/\/dl.acm.org\/citation.cfm?id=1882094.1882119"},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201910)","author":"Might Matthew","year":"2010","unstructured":"Matthew Might, Yannis Smaragdakis, and David Van Horn. 2010. Resolving and Exploiting the K-CFA Paradox: Illuminating Functional vs. Object-Oriented Program Analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201910). Association for Computing Machinery, New York, NY, USA. 305\u2013315. isbn:9781450300193 https:\/\/doi.org\/10.1145\/1806596.1806631 10.1145\/1806596.1806631"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_2_2_20_1","volume-title":"Mitchell and Krzysztof Apt","author":"John","year":"2003","unstructured":"John C. Mitchell and Krzysztof Apt. 2003. Concepts in Programming Languages. Cambridge University Press, USA. isbn:0521780985"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409001"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408984"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007734417713"},{"volume-title":"Control-flow Analysis of Higher-order Languages. Ph. D. Dissertation","author":"Shivers Olin Grigsby","key":"e_1_2_2_26_1","unstructured":"Olin Grigsby Shivers. 1991. Control-flow Analysis of Higher-order Languages. Ph. D. Dissertation. Pittsburgh, PA, USA. UMI Order No. GAX91-26964"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411243"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP\u201910)","author":"Vardoulakis Dimitrios","year":"2010","unstructured":"Dimitrios Vardoulakis and Olin Shivers. 2010. CFA2: A Context-Free Approach to Control-Flow Analysis. In Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP\u201910). Springer-Verlag, Berlin, Heidelberg. 570\u2013589. isbn:3-642-11956-5, 978-3-642-11956-9 https:\/\/doi.org\/10.1007\/978-3-642-11957-6_30 10.1007\/978-3-642-11957-6_30"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996859"},{"key":"e_1_2_2_31_1","unstructured":"Robert Zhang and Scott Smith. 2024. Open-Source Codebase for A Pure Demand Operational Semantics With Applications to Program Analysis. https:\/\/github.com\/JHU-PL-Lab\/dde"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Robert Zhang and Scott Smith. 2024. Software Artifact for A Pure Demand Operational Semantics With Applications to Program Analysis. https:\/\/doi.org\/10.5281\/zenodo.10794350 10.5281\/zenodo.10794350","DOI":"10.5281\/zenodo.10794350"},{"key":"e_1_2_2_33_1","unstructured":"Robert Zhang and Scott Smith. 2024. Software Artifact for A Pure Demand Operational Semantics With Applications to Program Analysis. https:\/\/archive.softwareheritage.org\/browse\/directory\/ffd5fe9eeca811865b5baa7183f2610105d056c0"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649852","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649852","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:07Z","timestamp":1750287247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":34,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649852"],"URL":"https:\/\/doi.org\/10.1145\/3649852","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}