解码Lua：面向开发者和语义学家的形式语义学
Decoding Lua: Formal Semantics for the Developer and the Semanticist
摘要：
我们在Lua程序设计语言的5.2版本中为它的一个大子集提供了形式语义。我们验证我们的模型，通过机械化它，并测试它对Lua的参考解释器的测试套件，确认我们的模型准确地代表了语言。此外，我们为自己设定了一个雄心勃勃的目标：目标是PL语义学家-不一定精通Lua-和Lua开发人员-不一定精通语义框架。对于前者，我们提出的语言的特点，以及我们如何在传统的小步操作语义，嵌入在Felleisen-Hieb的减少语义与评价上下文中建模。机械化自然是在PLT Redex中执行的，PLT Redex是用于机械化归约语义的事实上的工具。对于不熟悉这些概念的读者，我们提供了，在空间限制内尽可能好的，对模型的温和介绍。我们希望不同Lua实现和方言的开发人员能够理解该模型，并将其用于测试他们的工作和试验新的语言功能。
英文摘要：
We provide formal semantics for a large subset of the Lua programming language, in its version 5.2. We validate our model by mechanizing it and testing it against the test suite of the reference interpreter of Lua, confirming that our model accurately represents the language. In addition, we set us an ambitious goal: to target both a PL semanticist ---not necessarily versed in Lua---, and a Lua developer ---not necessarily versed in semantic frameworks. To the former, we present the peculiarities of the language, and how we model them in a traditional small-step operational semantics, embedded within Felleisen-Hieb's reduction semantics with evaluation contexts. The mechanization is, naturally, performed in PLT Redex, the de facto tool for mechanizing reduction semantics. To the reader unfamiliar with such concepts, we provide, to our best possible within the space limitations, a gentle introduction of the model. It is our hope that developers of the different Lua implementations and dialects understand the model and consider it both for testing their work and for experimenting with new language features.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
