Representing Structural Language Features in Formal Meta-languages
Representing Structural Language Features in Formal Meta-languages
复制标题
用形式元语言表示结构语言特征
DOI：
10.1007/978-3-030-53518-6_13
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
M. Kohlhase
中科院分区：
文献类型：
--
作者：
Dennis Müller;Florian Rabe;Colin Rothgang;M. Kohlhase
结构化语言功能是那些引入新类型声明的功能，而不是那些只添加表达式的功能。当用元语言（如OMDoc等标准格式或LF等逻辑框架）表示语言时，它们构成了一个重大挑战。希望使用浅层表示，其中结构语言特征由元语言的类似特征表示，但实际语言中结构语言特征的丰富性使得这很困难。因此，目前的技术水平是编码的不可表示的结构语言功能方面的更基本的，但这使得表示难以重用和验证。许多语言允许用户添加新的结构化语言功能，这些功能被精心设计到一个小型的可信内核中，从而允许大量且不断增长的功能集，这一事实加剧了这种挑战。
Structural language features are those that introduce new kinds of declarations as opposed to those that only add expressions. They pose a significant challenge when representing languages in meta-languages such as standard formats like OMDoc or logical frameworks like LF. It is desirable to use shallow representations where a structural language feature is represented by the analogous feature of the meta-language, but the richness of structural language features in practical languages makes this difficult. Therefore, the current state of the art is to encode unrepresentable structural language features in terms of more elementary ones, but that makes the representations difficult to reuse and verify. This challenge is exacerbated by the fact that many languages allow users to add new structural language features that are elaborated into a small trusted kernel, which allows for a large and growing set of features.
DOI：
10.1145/2951913.2951932
发表时间：
2016-09
期刊：
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
D. Christiansen;Edwin C. Brady
通讯作者：
D. Christiansen;Edwin C. Brady