Formal metatheory of second-order abstract syntax
Formal metatheory of second-order abstract syntax
复制标题
二阶抽象语法的形式元理论
DOI：
10.1145/3498715
复制
发表时间：
2022
影响因子：
--
通讯作者：
Fiore M
中科院分区：
文献类型：
--
作者：
Fiore M
尽管在理论和实践方面都进行了广泛的研究，但形式化，推理和实现具有变量绑定的语言仍然是一项艰巨的工作-重复的样板文件和过于复杂的捕获避免替换元理论经常阻碍语言的实际有趣属性。现有的发展提供了一些救济，但在代价的不便和容易出错的长期编码和缺乏正式的foundations.We提出了一个启发性的语言形式化框架中实现的Agda。该系统将具有变量绑定运算符的语法签名的描述转换为内部编码的归纳数据类型，该数据类型配备有语法操作，例如弱化和替换，沿着它们的正确性属性。所生成的元理论进一步结合了元变量及其相关的元替换操作，这使得二阶方程/重写推理。该框架的基础数学基础-初始代数语义-通过构造将语言的组合解释导出到满足语义替换引理的模型中。
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.
登录
查看更多内容
自由 Σ-monoids：带有元变量的高阶语法
DOI：
--
发表时间：
2004
期刊：
Proceedings of Second Asian Symposium on Programming Languages and Systems(APLAS'04) LNCS 3202
影响因子：
--
作者：
N.Ghani;M.Hamana;T.Uustalu;V.Vene;浜名誠;浜名誠;浜名誠
通讯作者：
浜名誠
模式同义词
DOI：
10.1145/2976002.2976013
发表时间：
2016
期刊：
Proceedings of the 9th International Symposium on Haskell
影响因子：
--
作者：
Matthew Pickering;Gergo Érdi;S. Jones;R. Eisenberg
通讯作者：
R. Eisenberg
简单类型理论的代数模型：多项式方法
DOI：
10.1145/3373718.3394771
发表时间：
2020
期刊：
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Nathanael Arkor;M. Fiore
通讯作者：
M. Fiore
替代：使用 Monad 和转换的形式方法案例研究
DOI：
10.1016/0167-6423(94)00022-0
发表时间：
1994
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
F. Bellegarde;J. Hook
通讯作者：
J. Hook
DOI：
10.1145/3018610.3018613
发表时间：
2017-01
期刊：
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
影响因子：
--
作者：
Guillaume Allais;James Chapman;Conor McBride;James McKinna
通讯作者：
Guillaume Allais;James Chapman;Conor McBride;James McKinna