一句话：将编译器计算技术推广到依赖类型设置，以支持类型化源语言并保证编译组件类型安全、便于机器验证。
编译器难以编写且难以保证正确。Bahr 与 Hutton 提出从正确性规约直接计算编译器，使编译器构造即正确，但此前仅适用于无类型源语言。本文把该技术扩展到依赖类型环境：利用依赖类型自然地表达类型化源语言及其编译正确性规约，确保所有编译组件类型安全，并使计算过程更容易在证明助手中进行机器检查。文章以函数式珍珠形式展示，表明依赖类型设置不仅支持类型化源语言，还提升正确性论证的可验证性，为构造即正确的类型化编译器提供了一条新路径。
Compilers are difficult to write, and difficult to get right. Bahr and Hutton recently developed a new technique for calculating compilers directly from specifications of their correctness, which ensures that the resulting compilers are correct-by-construction. To date, however, this technique has only been applicable to source languages that are untyped. In this article, we show that moving to a dependently-typed setting allows us to naturally support typed source languages, ensure that all compilation components are type-safe, and make the resulting calculations easier to mechanically check using a proof assistant.
@article{paperbot1128,
title = {Calculating dependently-typed compilers (functional pearl)},
author = {Mitchell Pickard and Graham Hutton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473587}
}