一句话：在 Agda 中基于初始代数语义自动生成带变量绑定与二阶替换的语言元理论框架。
该论文针对带变量绑定的语言在形式化、推理与实现中长期存在的重复样板和捕获避免替换元理论过于复杂的问题，提出一个受数学启发的语言形式化框架，并在 Agda 中实现。框架将带绑定算子的语法签名描述翻译为内在编码的归纳数据类型，自动配备 weakening、substitution 等语法操作及其正确性性质，并进一步集成 metavariable 与 metasubstitution，从而支持二阶等式与重写推理。其数学基础是初始代数语义，能够按构造导出语言的组合语义解释，并保证其模型满足语义替换引理。相较既有方案，该工作避免了不便且易错的项编码，同时提供了形式化基础。
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour – repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning. The underlying mathematical foundation of the framework – initial algebra semantics – derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.
@article{paperbot1577,
title = {Formal metatheory of second-order abstract syntax},
author = {Marcelo Fiore and Dmitrij Szamozvancev},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498715}
}