一句话：提出延迟替换技术，为 Nix 等动态语言给出小型步操作语义与环境解释器，并在 Rocq 中机器化验证其可靠性与完备性。
动态/脚本语言（如 JavaScript、PHP、Nix）的语义规范常需同时给出基于替换的小步操作语义与基于环境的解释器，但证明二者对应关系十分困难。本文以具有变量与属性成员重载、隐蔽遮蔽、混合求值策略和复杂递归等特性的 Nix 表达式语言为对象，从按名调用 lambda 演算逐步扩展到含动态变量名与动态绑定名的核心演算，再到 Nix。核心创新是延迟替换（deferred substitutions），它为动态变量绑定给出简洁的基于替换的语义；作者构造对应环境解释器，并证明其在终止、出错与发散程序上相对于操作语义可靠且完备。全部结果在 Rocq 中机器化，利用 Rocq-std++ 新特性表示递归位置含 map 的语法；再经 extraction 生成可执行 OCaml 解释器，在官方 Nix 语言测试上运行，给出迄今最全面的 Nix 形式语义。
To study the semantics of a programming language, it is useful to consider different specification forms— e.g ., a substitution-based small-step operational semantics and an environment-based interpreter—because they have mutually exclusive benefits. Developing these specifications and proving correspondences is challenging for ‘dynamic’/‘scripting’ 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. 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 deferred substitutions , 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. 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’s extraction mechanism to turn our Nix interpreter into executable OCaml code, which we apply to the official Nix language tests. Altogether this gives rise to the most comprehensive formal semantics for the Nix expression language to date.
@article{paperbot3059,
title = {Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language},
author = {Rutger Broekhoff and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747537}
}