This paper concerns the development of metatheory for extensible languages. It uses as its starting point a view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In the elaboration of this perspective, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented in this context by formulas over such relations. These properties may be fundamental to the language, introduced by the host language, or they may pertain to analyses introduced by individual extensions. We expose the problem of modular metatheory, i.e., the notion that proofs of relevant properties can be constructed by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Mathematical precision is given to our discussions by framing them within a logic that encodes inductive rule-based specifications via least fixed-point definitions. We also sketch the structure of a practical system for metatheoretic reasoning for extensible languages based on the ideas developed.

翻译：本文关注可扩展语言的元理论发展。其出发点是将面向特定应用领域的编程语言视为通过组合来自宿主语言独立开发扩展的开源库中的组件来构建。在这一视角的阐述中，静态分析（如类型检查）和动态语义（如求值）通过关系来描述，这些关系的规范分布在宿主语言和扩展中，并以基于规则的方式给出。确保静态分析准确衡量运行时行为的元理论性质，在此上下文中由这些关系上的公式表示。这些性质可能是语言固有的、由宿主语言引入的，也可能与单个扩展引入的分析相关。我们揭示了模块化元理论的问题，即相关性质的证明可以通过在库中每个组件内独立推理来构建的概念。为解决这一问题，我们提出了围绕语言片段分解证明以及基于对其行为施加的广泛先验约束对扩展进行通用推理的双重思路。我们通过展示如何对于通过组合独立部分得到的任意语言自动构建属性的完整证明，来确立这些推理风格的有效性。通过将讨论置于一个通过最小不动点定义对归纳规则规范进行编码的逻辑框架内，我们赋予了讨论数学精确性。我们还基于所提出的思想，勾勒了一个用于可扩展语言元理论推理的实用系统的结构。