Intrinsically-typed definitional interpreters à la carte
Intrinsically-typed definitional interpreters à la carte
复制标题
本质类型定义解释器 à la carte
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Peter D. Mosses
中科院分区：
文献类型：
--
作者：
Cas van der Rest;Casper Bach Poulsen;A. Rouvoet;E. Visser;Peter D. Mosses
对类型安全的编程语言进行验证和机械验证需要大量的工作。理论上，通过定义和重用预先验证的模块化组件，可以减少这种工作量。然而，在实践中，现有的模块化机械验证方法需要的规范代码是普通的单片定义的许多倍。这使得开发新的可重用组件变得困难，并且使得现有的组件规范难以掌握。我们提出了一种替代方法的基础上，内在类型的解释器，它减少了规模和复杂性的模块化规范相比，现有的方法。此外，我们为预验证的类型安全语言组件的构造安全规范和组合引入了一个新的抽象：语言片段。语言片段与简单的、单一的内在类型解释器一样简洁和易于开发，但所需的代码比以前的类型安全模块化机械验证方法少10倍。
Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
登录
查看更多内容
轻柔的悬浮艺术
影响因子：
--
作者：
Chapman J
通讯作者：
Chapman J
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter
DOI：
10.1145/2577080.2577099
发表时间：
2014
期刊：
--
影响因子：
--
作者：
Churchill M
通讯作者：
Churchill M
影响因子：
--
作者：
Dagand P
通讯作者：
Dagand P