{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:12Z","timestamp":1780994712270,"version":"3.54.1"},"reference-count":94,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>This paper makes a first step towards a formal definition of OCaml and a foundational program verification environment for OCaml. We present a formal definition of OLang, a nontrivial sequential fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers. We define the dynamic semantics of OLang as a monadic interpreter. This interpreter runs atop a custom monad where computations are internally represented as trees of operations and equipped with a small-step semantics. We define two program logics for OLang. A stateless Hoare Logic allows reasoning about so-called \"pure\" programs; an Iris-based Separation Logic allows reasoning about arbitrary programs. We present the construction of the two logics as well as some examples of their use.<\/jats:p>","DOI":"10.1145\/3747509","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"128-159","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Semantics and Program Logics for a Fragment of OCaml"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6226-1413","authenticated-orcid":false,"given":"Remy","family":"Seassau","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3388-1257","authenticated-orcid":false,"given":"Irene","family":"Yoon","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2723-8418","authenticated-orcid":false,"given":"Jean-Marie","family":"Madiot","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the ACM on Programming Languages, 9, POPL (2025","author":"Allain Cl\u00e9ment","year":"2025","unstructured":"Cl\u00e9ment Allain, Fr\u00e9d\u00e9ric Bour, Basile Cl\u00e9ment, Fran\u00e7ois Pottier, and Gabriel Scherer. 2025. Tail Modulo Cons, OCaml, and Relational Separation Logic. Proceedings of the ACM on Programming Languages, 9, POPL (2025), Jan., 2337\u20132363. http:\/\/cambium.inria.fr\/~fpottier\/publis\/tmc-popl2025.pdf"},{"key":"e_1_2_1_2_1","unstructured":"L\u00e9o Andr\u00e8s Pierre Chambart and Jean-Christophe Filli\u00e2tre. 2023. Wasocaml: compiling OCaml to WebAssembly. In Implementation of Functional Languages (IFL). https:\/\/inria.hal.science\/hal-04311345"},{"key":"e_1_2_1_3_1","volume-title":"Verified Software Toolchain. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"17","author":"Appel Andrew W.","year":"2011","unstructured":"Andrew W. Appel. 2011. Verified Software Toolchain. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 6602). Springer, 1\u201317. https:\/\/www.cs.princeton.edu\/~appel\/papers\/vst.pdf"},{"key":"e_1_2_1_4_1","volume-title":"Vellvm: Formalizing the\u00a0Informal LLVM. In NASA Formal Methods (NFM)","author":"Beck Calvin","year":"2025","unstructured":"Calvin Beck, Hanxi Chen, and Steve Zdancewic. 2025. Vellvm: Formalizing the\u00a0Informal LLVM. In NASA Formal Methods (NFM). Springer, 91\u201399. https:\/\/www.cis.upenn.edu\/~stevez\/papers\/nfm25.pdf"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the ACM on Programming Languages, 3, OOPSLA (2019","author":"Bender John","year":"2019","unstructured":"John Bender and Jens Palsberg. 2019. A formalization of Java\u2019s concurrent access modes. Proceedings of the ACM on Programming Languages, 3, OOPSLA (2019), 142:1\u2013142:28. https:\/\/johnbender.us\/assets\/oopsla-2019.pdf"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Martin Bodin Arthur Chargu\u00e9raud Daniele Filaretti Philippa Gardner Sergio Maffeis Daiva Naudziuniene Alan Schmitt and Gareth Smith. 2014. A trusted mechanised JavaScript specification. In Principles of Programming Languages (POPL). 87\u2013100. https:\/\/www.chargueraud.org\/research\/2013\/js\/jscert_popl.pdf","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290357"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs","volume":"61","author":"Cao Qinxiang","year":"2018","unstructured":"Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61, 1-4 (2018), 367\u2013422. https:\/\/www.cs.princeton.edu\/~appel\/papers\/VST-Floyd.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_10_1","volume-title":"Workshop on Coq for Programming Languages. https:\/\/people.csail.mit.edu\/nickolai\/papers\/chajed-goose-coqpl.pdf","author":"Chajed Tej","year":"2020","unstructured":"Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2020. Verifying concurrent Go code in Coq with Goose. In Workshop on Coq for Programming Languages. https:\/\/people.csail.mit.edu\/nickolai\/papers\/chajed-goose-coqpl.pdf"},{"key":"e_1_2_1_11_1","volume-title":"Symposium on Operating Systems Design and Implementation. 423\u2013439","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In Symposium on Operating Systems Design and Implementation. 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"key":"e_1_2_1_13_1","volume-title":"Program Verification Through Characteristic Formulae. In International Conference on Functional Programming (ICFP). 321\u2013332","author":"Chargu\u00e9raud Arthur","year":"2010","unstructured":"Arthur Chargu\u00e9raud. 2010. Program Verification Through Characteristic Formulae. In International Conference on Functional Programming (ICFP). 321\u2013332. http:\/\/www.chargueraud.org\/research\/2010\/cfml\/main.pdf"},{"key":"e_1_2_1_14_1","volume-title":"Characteristic Formulae for the Verification of Imperative Programs. In International Conference on Functional Programming (ICFP). 418\u2013430","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). 418\u2013430. http:\/\/www.chargueraud.org\/research\/2011\/cfml\/main.pdf"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2022\/6\/13"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the ACM on Programming Languages, 5, POPL","author":"de Vilhena Paulo Em\u00edlio","year":"2021","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. A Separation Logic for Effect Handlers. Proceedings of the ACM on Programming Languages, 5, POPL (2021), Jan., http:\/\/cambium.inria.fr\/~fpottier\/publis\/de-vilhena-pottier-sleh.pdf"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Chucky Ellison and Grigore Rosu. 2012. An executable formal semantics of C with applications. In Principles of Programming Languages (POPL). 533\u2013544. https:\/\/fsl.cs.illinois.edu\/publications\/ellison-rosu-2012-popl.pdf","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_1_20_1","volume-title":"Semi-automated Reasoning About Non-determinism in C Expressions. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"87","author":"Frumin Dan","year":"2019","unstructured":"Dan Frumin, L\u00e9on Gondelman, and Robbert Krebbers. 2019. Semi-automated Reasoning About Non-determinism in C Expressions. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 11423). Springer, 60\u201387. https:\/\/iris-project.org\/pdfs\/2019-esop-c.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010095604496"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010043619517"},{"key":"e_1_2_1_24_1","volume-title":"Computer Aided Verification (CAV) (Lecture Notes in Computer Science","volume":"10","author":"Gardner Philippa","year":"2015","unstructured":"Philippa Gardner, Gareth Smith, Conrad Watt, and Thomas Wood. 2015. A Trusted Mechanised Specification of JavaScript: One Year On. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 9206). Springer, 3\u201310. https:\/\/www.doc.ic.ac.uk\/~pg\/publications\/Gardner2015Trusted.pdf"},{"key":"e_1_2_1_25_1","volume-title":"International Conference on Functional Programming (ICFP). 339\u2013347","author":"Gibbons Jeremy","year":"2014","unstructured":"Jeremy Gibbons and Nicolas Wu. 2014. Folding domain-specific languages: deep and shallow embeddings (functional Pearl). In International Conference on Functional Programming (ICFP). 339\u2013347. https:\/\/www.cs.ox.ac.uk\/jeremy.gibbons\/publications\/embedding.pdf"},{"key":"e_1_2_1_26_1","volume-title":"Verified Characteristic Formulae for CakeML. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"610","author":"Gu\u00e9neau Arma\u00ebl","year":"2017","unstructured":"Arma\u00ebl Gu\u00e9neau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. 2017. Verified Characteristic Formulae for CakeML. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 10201). Springer, 584\u2013610. http:\/\/cambium.inria.fr\/~agueneau\/publis\/gueneau-myreen-kumar-norrish-cf-cakeml.pdf"},{"key":"e_1_2_1_27_1","unstructured":"Robert Harper and Karl Crary. 2014. The Mechanization of Standard ML. Feb. https:\/\/github.com\/SMLFamily\/The-Mechanization-of-Standard-ML Available online"},{"key":"e_1_2_1_28_1","unstructured":"Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. Department of Computer Science Katholieke Universiteit Leuven. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/verifast.pdf"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_32_1","volume-title":"Haskell symposium. 94\u2013105","author":"Kiselyov Oleg","year":"2015","unstructured":"Oleg Kiselyov and Hiromi Ishii. 2015. Freer monads, more extensible effects. In Haskell symposium. 94\u2013105. https:\/\/okmij.org\/ftp\/Haskell\/extensible\/more.pdf"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers. 2014. An operational and axiomatic semantics for non-determinism and sequence points in C. In Principles of Programming Languages (POPL). 101\u2013112. https:\/\/doi.org\/10.1145\/2535838.2535878 10.1145\/2535838.2535878","DOI":"10.1145\/2535838.2535878"},{"key":"e_1_2_1_35_1","volume-title":"The C standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","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_2_1_36_1","volume-title":"Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science","volume":"548","author":"Krebbers Robbert","year":"2014","unstructured":"Robbert Krebbers, Xavier Leroy, and Freek Wiedijk. 2014. Formal C Semantics: CompCert and the C Standard. In Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science, Vol. 8558). Springer, 543\u2013548. https:\/\/robbertkrebbers.nl\/research\/articles\/compcert_formalin.pdf"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: a verified implementation of ML. In Principles of Programming Languages (POPL). 179\u2013192. https:\/\/cakeml.org\/popl14.pdf","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In Programming Language Design and Implementation (PLDI). 618\u2013632. https:\/\/plv.mpi-sws.org\/scfix\/paper.pdf","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_39_1","unstructured":"Isabella Leandersson. 2022. Six Surprising Reasons the OCaml Programming Language is Good for Business. https:\/\/tarides.com\/blog\/2022-11-22-six-surprising-reasons-the-ocaml-programming-language-is-good-for-business\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Daniel K. Lee Karl Crary and Robert Harper. 2007. Towards a mechanized metatheory of Standard ML. In Principles of Programming Languages (POPL). 173\u2013184. https:\/\/www.cs.cmu.edu\/~dklee\/papers\/tslf-popl.pdf","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Principles of Programming Languages (POPL). 42\u201354. http:\/\/cambium.inria.fr\/~xleroy\/publi\/compiler-certif.pdf","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_44_1","unstructured":"Xavier Leroy. 2024. The CompCert C compiler. http:\/\/compcert.org\/"},{"key":"e_1_2_1_45_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2024. The OCaml system. https:\/\/ocaml.org\/manual\/"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_2_1_48_1","volume-title":"Machine-Checked Formalisation. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"517","author":"Lochbihler Andreas","year":"2012","unstructured":"Andreas Lochbihler. 2012. Java and the Java Memory Model \u2013 A Unified, Machine-Checked Formalisation. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 7211). Springer, 497\u2013517. https:\/\/ethz.ch\/content\/dam\/ethz\/special-interest\/infk\/inst-infsec\/information-security-group-dam\/people\/andreloc\/lochbihler12esop.pdf"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386336"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_2_1_51_1","volume-title":"Adve","author":"Manson Jeremy","year":"2005","unstructured":"Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java memory model. In Principles of Programming Languages (POPL). 378\u2013391. http:\/\/rsim.cs.uiuc.edu\/Pubs\/popl05.pdf"},{"key":"e_1_2_1_52_1","volume-title":"Mathematics of Program Construction (MPC) (Lecture Notes in Computer Science","volume":"275","author":"McBride Conor","year":"2015","unstructured":"Conor McBride. 2015. Turing-Completeness Totally Free. In Mathematics of Program Construction (MPC) (Lecture Notes in Computer Science, Vol. 9129). Springer, 257\u2013275. https:\/\/strathprints.strath.ac.uk\/60166\/1\/McBride_LNCS2015_Turing_completeness_totally_free.pdf"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_54_1","volume-title":"The Definition of Standard ML (Revised)","author":"Milner Robin","unstructured":"Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML (Revised). MIT Press. https:\/\/smlfamily.github.io\/sml97-defn.pdf"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571218"},{"key":"e_1_2_1_56_1","unstructured":"Antonio Vinhas Nunes Monteiro. 2025. Melange. https:\/\/github.com\/melange-re\/melange"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.1"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, ICFP (2020","author":"M\u00e9vel Glen","year":"2020","unstructured":"Glen M\u00e9vel, Jacques-Henri Jourdan, and Fran\u00e7ois Pottier. 2020. Cosmo: A Concurrent Separation Logic for Multicore OCaml. Proceedings of the ACM on Programming Languages, 4, ICFP (2020), June, http:\/\/cambium.inria.fr\/~fpottier\/publis\/mevel-jourdan-pottier-cosmo-2020.pdf"},{"key":"e_1_2_1_59_1","volume-title":"C formalised in HOL","author":"Norrish Michael","unstructured":"Michael Norrish. 1998. C formalised in HOL. University of Cambridge. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-453.pdf"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.024"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_1"},{"key":"e_1_2_1_62_1","volume-title":"Functional Big-Step Semantics. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"615","author":"Owens Scott","year":"2016","unstructured":"Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 9632). Springer, 589\u2013615. https:\/\/cakeml.org\/esop16.pdf"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622814"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.32"},{"key":"e_1_2_1_66_1","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2015.12.003","article-title":"An Introduction to Algebraic Effects and Handlers","volume":"319","author":"Pretnar Matija","year":"2015","unstructured":"Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Electronic Notes in Theoretical Computer Science, 319 (2015), 19\u201335. http:\/\/www.eff-lang.org\/handlers-tutorial.pdf","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1002\/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4","article-title":"Objective ML: An effective object-oriented extension to ML","volume":"4","author":"R\u00e9my Didier","year":"1998","unstructured":"Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 1998. Objective ML: An effective object-oriented extension to ML. Theory and Practice of Object Systems, 4, 1 (1998), 27\u201350. http:\/\/cambium.inria.fr\/~remy\/ftp\/objective-ml!tapos98.pdf","journal-title":"Theory and Practice of Object Systems"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In Programming Language Design and Implementation (PLDI). 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","unstructured":"Remy Seassau Irene Yoon Jean-Marie Madiot and Fran\u00e7ois Pottier. 2025. Formal Semantics and Program Logics for a Fragment of OCaml - Artifact. https:\/\/doi.org\/10.5281\/zenodo.16327523 10.5281\/zenodo.16327523","DOI":"10.5281\/zenodo.16327523"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408995"},{"key":"e_1_2_1_74_1","doi-asserted-by":"crossref","unstructured":"K. C. Sivaramakrishnan Stephen Dolan Leo White Tom Kelly Sadiq Jaffer and Anil Madhavapeddy. 2021. Retrofitting effect handlers onto OCaml. In Programming Language Design and Implementation (PLDI). 206\u2013221. arxiv:2104.00250","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_2_1_75_1","volume-title":"Context-Dependent Effects in Guarded Interaction Trees. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science). Springer. https:\/\/iris-project.org\/pdfs\/2025-esop-gitrees.pdf","author":"Stepanenko Sergei","year":"2025","unstructured":"Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, and Lars Birkedal. 2025. Context-Dependent Effects in Guarded Interaction Trees. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science). Springer. https:\/\/iris-project.org\/pdfs\/2025-esop-gitrees.pdf"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_124"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_2_1_79_1","unstructured":"The Osiris Project. 2025. Osiris. https:\/\/gitlab.inria.fr\/fpottier\/osiris"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704841"},{"key":"e_1_2_1_81_1","volume-title":"Higher Order Logic Theorem Proving and its Applications (HUG) (Lecture Notes in Computer Science","author":"VanInwegen Myra","unstructured":"Myra VanInwegen and Elsa Gunter. 1993. HOL-ML. In Higher Order Logic Theorem Proving and its Applications (HUG) (Lecture Notes in Computer Science, Vol. 780). Springer, 61\u201374. https:\/\/link.springer.com\/chapter\/10.1007\/3-540-57826-9_125"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704847"},{"key":"e_1_2_1_83_1","unstructured":"J\u00e9r\u00f4me Vouillon. 2023. wasm_of_ocaml. https:\/\/cambium.inria.fr\/seminaires\/transparents\/20231213.Jerome.Vouillon.pdf Slides"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2187"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689780"},{"key":"e_1_2_1_86_1","volume-title":"Mechanising and evolving the formal semantics of WebAssembly: the Web\u2019s new low-level language. Ph. D. Dissertation","author":"Watt Conrad","unstructured":"Conrad Watt. 2021. Mechanising and evolving the formal semantics of WebAssembly: the Web\u2019s new low-level language. Ph. D. Dissertation. University of Cambridge. https:\/\/www.repository.cam.ac.uk\/items\/96441ace-e88d-4709-8490-296ce668b228"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.9"},{"key":"e_1_2_1_88_1","volume-title":"Formal Methods (FM) (Lecture Notes in Computer Science","volume":"79","author":"Watt Conrad","year":"2021","unstructured":"Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 13047). Springer, 61\u201379. https:\/\/hal.science\/hal-03353748"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591224"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_91_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Zakowski Yannick","year":"2020","unstructured":"Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages, 4, POPL (2020), 51:1\u201351:32. https:\/\/www.cis.upenn.edu\/~stevez\/papers\/XZHH+20.pdf"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547630"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_2_1_94_1","doi-asserted-by":"crossref","unstructured":"Jianzhou Zhao Santosh Nagarakatte Milo M. K. Martin and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In Principles of Programming Languages (POPL). 427\u2013440. https:\/\/www.cis.upenn.edu\/~stevez\/papers\/ZNMZ12.pdf","DOI":"10.1145\/2103656.2103709"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747509","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:58:19Z","timestamp":1754413099000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747509"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":94,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747509"],"URL":"https:\/\/doi.org\/10.1145\/3747509","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}