{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:27:46Z","timestamp":1755217666979,"version":"3.43.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"name":"ERC","award":["101171349"],"award-info":[{"award-number":["101171349"]}]}],"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>\n            To study the semantics of a programming language, it is useful to consider different specification forms\u2014\n            <jats:italic toggle=\"yes\">e.g.<\/jats:italic>\n            , a substitution-based small-step operational semantics and an environment-based interpreter\u2014because they have mutually exclusive benefits. Developing these specifications and proving correspondences is challenging for \u2018dynamic\u2019\/\u2018scripting\u2019 languages such as JavaScript, PHP and Bash. We study this challenge in the context of the Nix expression language, a dynamic language used in the eponymous package manager and operating system. Nix is a Turing-complete, untyped functional language designed for the manipulation of JSON-style attribute sets, with tricky features such as overloaded use of variables for lambda bindings and attribute members, subtle shadowing rules, a mixture of evaluation strategies, and tricky mechanisms for recursion.\n          <\/jats:p>\n          <jats:p>\n            We show that our techniques are applicable beyond Nix by starting from the call-by-name lambda calculus, which we extend to a core lambda calculus with dynamically computed variable names and dynamic binder names, and finally to Nix. Our key novelty is the use of a form of\n            <jats:italic toggle=\"yes\">deferred substitutions<\/jats:italic>\n            , which enables us to give a concise substitution-based semantics for dynamic variable binding. We develop corresponding environment-based interpreters, which we prove to be sound and complete (for terminating, faulty and diverging programs) w.r.t. our operational semantics based on deferred substitutions.\n          <\/jats:p>\n          <jats:p>We mechanize all our results in the Rocq prover and showcase a new feature of the Rocq-std++ library for representing syntax with maps in recursive positions. We use Rocq\u2019s extraction mechanism to turn our Nix interpreter into executable OCaml code, which we apply to the official Nix language tests.  \nAltogether this gives rise to the most comprehensive formal semantics for the Nix expression language to date.<\/jats:p>","DOI":"10.1145\/3747537","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"917-946","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3716-5638","authenticated-orcid":false,"given":"Rutger","family":"Broekhoff","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. 666\u2013679. https:\/\/doi.org\/10.1145\/3009837.3009866 10.1145\/3009837.3009866","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-022-09655-X"},{"key":"e_1_2_1_5_1","unstructured":"Anton Bachin. 2023. Bisect_ppx. https:\/\/github.com\/aantron\/bisect_ppx"},{"volume-title":"The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics","author":"Barendregt Hendrik Pieter","key":"e_1_2_1_6_1","unstructured":"Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics, Vol. 103). North-Holland. isbn:978-0-444-86748-3"},{"key":"e_1_2_1_7_1","unstructured":"Martin Bodin. 2016. Certified semantics and analysis of JavaScript. Ph. D. Dissertation. Universit\u00e9 Rennes 1 France."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Martin Bodin Arthur Chargu\u00e9raud Daniele Filaretti Philippa Gardner Sergio Maffeis Daiva Naud\u017ei\u016bnien\u0117 Alan Schmitt and Gareth Smith. 2014. A trusted mechanised JavaScript specification. In POPL. 87\u2013100. https:\/\/doi.org\/10.1145\/2535838.2535876 10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Rutger Broekhoff and Robbert Krebbers. 2025. Artifact for \u201cVerified interpreters for dynamic languages with applications to the Nix expression language\u201d. https:\/\/doi.org\/10.5281\/zenodo.15839106 10.5281\/zenodo.15839106","DOI":"10.5281\/zenodo.15839106"},{"key":"e_1_2_1_11_1","volume-title":"Nix with","author":"Caddet Fran\u00e7ois","year":"2023","unstructured":"Fran\u00e7ois Caddet. 2023. Nix with; with Nickel. https:\/\/tweag.io\/blog\/2023-01-24-nix-with-with-nickel\/"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_8"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9225-2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_1_16_1","volume-title":"The purely functional software deployment model. Ph. D. Dissertation","author":"Dolstra Eelco","year":"1874","unstructured":"Eelco Dolstra. 2006. The purely functional software deployment model. Ph. D. Dissertation. Utrecht University, Netherlands. http:\/\/dspace.library.uu.nl\/handle\/1874\/7540"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Eelco Dolstra and Andres L\u00f6h. 2008. NixOS: A purely functional Linux distribution. In ICFP. 367\u2013378. https:\/\/doi.org\/10.1145\/1411204.1411255 10.1145\/1411204.1411255","DOI":"10.1145\/1411204.1411255"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000195"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_23"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/S001650200016"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Philippa Gardner Sergio Maffeis and Gareth David Smith. 2012. Towards a program logic for JavaScript. In POPL. 31\u201344. https:\/\/doi.org\/10.1145\/2103656.2103663 10.1145\/2103656.2103663","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371111"},{"key":"e_1_2_1_24_1","unstructured":"Arjun Guha Claudiu Saftoiu Spiridon Eliopoulos Benjamin Lerner and Joe Gibbs Politz. 2013. The LambdaJS GitHub repository. https:\/\/github.com\/brownplt\/LambdaJS"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_2_1_26_1","unstructured":"Ryan Hendrickson. 2024. Nix Pull Request #11294 parser-state: fix attribute merging. https:\/\/github.com\/NixOS\/nix\/pull\/11294"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_29_1","unstructured":"Adam Khayam Louis Noizet and Alan Schmitt. 2021. JSkel: Towards a Formalization of JavaScript\u2019s Semantics. In JFLA. 95\u2013116. https:\/\/inria.hal.science\/hal-03509431"},{"key":"e_1_2_1_30_1","unstructured":"Denis Korzunov. 2018. A Nix code formatter written in OCaml using Menhir and OCamllex. https:\/\/github.com\/d2km\/nixformat\/"},{"volume-title":"The C standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","key":"e_1_2_1_31_1","unstructured":"Robbert Krebbers. 2015. The C standard formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen, Netherlands."},{"key":"e_1_2_1_32_1","unstructured":"Robbert Krebbers. 2023. Efficient Extensional and Generic Finite Maps in Coq-std++. https:\/\/coq-workshop.gitlab.io\/2023\/abstracts\/coq2023_finmap-stdpp.pdf Extended abstract at \u201cThe Coq Workshop 2023\u201d see also"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10990-007-9018-9"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_2_1_37_1","unstructured":"Ben Lippmeier. 2016. Don\u2019t Substitute into Abstractions. https:\/\/benl.ouroborus.net\/papers\/2016-dsim\/lambda-dsim-20160328.pdf Unpublished manuscript"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_17"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_2_1_40_1","unstructured":"Marek Materzok. 2016. Certified Desugaring of JavaScript Programs using Coq. Presented at CoqPL\u201916. http:\/\/arthur.chargueraud.org\/events\/coqpl2016\/CoqPL_2016_paper_3.pdf"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Karl Mazurak and Steve Zdancewic. 2007. ABASH: finding bugs in bash scripts. In PLAS. 105\u2013114. https:\/\/doi.org\/10.1145\/1255329.1255347 10.1145\/1255329.1255347","DOI":"10.1145\/1255329.1255347"},{"key":"e_1_2_1_42_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. Digital Technical Journal, 10, 1 (1998), 100\u2013107. https:\/\/www.hpl.hp.com\/hpjournal\/dtj\/vol10num1\/vol10num1art9.pdf","journal-title":"Digital Technical Journal"},{"key":"e_1_2_1_43_1","unstructured":"Alexey Muranov. 2017. Nix issue #1361 Language feature proposal: exclusive \u2018with\u2019. https:\/\/github.com\/NixOS\/nix\/issues\/1361"},{"key":"e_1_2_1_44_1","volume-title":"An infrastructure for tractable verification of JavaScript programs. Ph. D. Dissertation","author":"Naud\u017ei\u016bnien\u0117 Daiva","year":"2018","unstructured":"Daiva Naud\u017ei\u016bnien\u0117. 2018. An infrastructure for tractable verification of JavaScript programs. Ph. D. Dissertation. Imperial College London, UK. https:\/\/vtss.doc.ic.ac.uk\/publications\/Naudziuniene2018Infrastructure.pdf"},{"key":"e_1_2_1_45_1","unstructured":"NixOS contributors. 2025. The Nix GitHub repository. https:\/\/github.com\/NixOS\/nix\/tree\/2.25.0"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Daejun Park Andrei Stef\u0103nescu and Grigore Ro\u015fu. 2015. KJS: a complete formal semantics of JavaScript. In PLDI. 346\u2013356. https:\/\/doi.org\/10.1145\/2737924.2737991 10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","key":"e_1_2_1_47_1","unstructured":"Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In PLDI. 199\u2013208. https:\/\/doi.org\/10.1145\/53990.54010 10.1145\/53990.54010","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_1_49_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2024","unstructured":"Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey. 2024. Programming Language Foundations. In Software Foundations, Benjamin C. Pierce (Ed.). https:\/\/softwarefoundations.cis.upenn.edu\/plf-current\/index.html"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Joe Gibbs Politz Matthew J. Carroll Benjamin S. Lerner Justin Pombrio and Shriram Krishnamurthi. 2012. A tested semantics for getters setters and eval in JavaScript. In DLS. 1\u201316. https:\/\/doi.org\/10.1145\/2384577.2384579 10.1145\/2384577.2384579","DOI":"10.1145\/2384577.2384579"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158138"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290379"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2019.29"},{"key":"e_1_2_1_54_1","unstructured":"Jude Taylor. 2015. Nix issue #490 Scoping is unintuitive. https:\/\/github.com\/NixOS\/nix\/issues\/490"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Jianzhou Zhao Santosh Nagarakatte Milo M. K. Martin and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In POPL. 427\u2013440. https:\/\/doi.org\/10.1145\/2103656.2103709 10.1145\/2103656.2103709","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\/3747537","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:24Z","timestamp":1754412984000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747537"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":55,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747537"],"URL":"https:\/\/doi.org\/10.1145\/3747537","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}