一句话：提出基于内在类型化解释器的语言片段抽象，以低代码量实现类型安全语言组件的模块化机械验证。
机械验证类型安全编程语言需要大量规约工作；现有模块化验证方法虽可复用预验证组件，却往往比单体定义多出数倍规约代码，难以开发和理解。本文提出基于内在类型化定义式解释器的替代方案，通过将类型信息内置于解释器语法中，降低模块化规约的规模与复杂度。作者进一步引入“语言片段”（language fragments）抽象，用于安全构造式地规约和组合预验证的类型安全语言组件，使组件像单体内在类型化解释器一样简洁易写，同时代码量约为此前模块化类型安全机械验证方法的十分之一。
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.
@article{paperbot1427,
title = {Intrinsically-typed definitional interpreters à la carte},
author = {Cas van der Rest and Casper Bach Poulsen and Arjen Rouvoet and Eelco Visser and Peter Mosses},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563355}
}