一句话：提出基于环境的小步语义 λE，避免替换，自然支持一等环境并具 Coq 形式化。
该文主张用语境（environment）而非替换来形式化编程语言语义，以更贴近实现并简化绑定问题。作者提出按值调用、静态类型的 λE 演算，采用小步环境语义与 de Bruijn 索引；它保守扩展 STLC，并几乎自然地引入一等环境，从而获得传统 λ 演算不具备的表达力。作者给出实现该语义的抽象机及其正确性证明，扩展引用，并用一等环境建模简单一等模块与能力。所有技术结果在 Coq 中形式化。结果表明该风格有三项正交收益：简化形式化与证明助手中的绑定问题、更贴近实现、以近乎零额外成本获得一等环境的表达力。
Formalizations of programming languages typically adopt the substitution model from the lambda calculus. However, substitution creates notorious complications for reasoning and implementation. Furthermore, it is disconnected from practical implementations, which normally adopt environments and closures. In this paper we advocate for formalizing programming languages using a novel style of small-step environment-based semantics , which avoids substitution and is closer to implementations. We present a call-by-value statically typed calculus, called λ E , using our small-step environment semantics. With our alternative environment semantics programming language constructs for first-class environments arise naturally, without creating significant additional complexity. Therefore, λ E also adopts first-class environments, adding expressive power that is not available in conventional lambda calculi. λ E is a conservative extension of the call-by-value Simply Typed Lambda Calculus (STLC), and employs de Bruijn indices for its formalization, which fit naturally with the environment-based semantics. Reasoning about λ E is simple, and in many cases simpler than reasoning about the traditional STLC. We show an abstract machine that implements the semantics of λ E , and has an easy correctness proof. We also extend λ E with references. We show that λ E can model a simple form of first-class modules, and suggest using first-class environments as an alternative to objects for modelling capabilities. All technical results are formalized in the Coq proof assistant. In summary, our work shows that the small-step environment semantics that we adopt has three main and orthogonal benefits: 1) it simplifies the notorious binding problem in formalizations and proof assistants; 2) it is closer to implementations; and 3) additional expressive power is obtained from first-class environments almost for free.