一句话：提出 skew bisimilarity，放宽编译器正确性规约，使计算编译器时可安全忽略源语言的不安全行为。
编译器计算（compiler calculation）从正确性规约出发推导“构造即正确”的编译器，规约通常要求源与目标程序语义双相似（bisimilarity）。但对含不安全行为的复杂源语言，全程双相似过强，现有计算技术无法处理这种部分规约。本文提出双相似的推广 skew bisimilarity，允许在计算编译器时安全忽略不安全行为以放宽规约；对安全源程序仍保持强正确性保证，并可产出更高效的目标代码。即使源语言无不安全行为，它也为寄存器机推理提供新的计算技术，突破以往仅适用于无效应、可终止源语言的限制。作者在 Agda 中完整形式化，为多种语言计算编译器，包括首个面向寄存器机的带类型并发 lambda 演算编译器。
Compiler calculation is a technique for deriving a correct-by-construction compiler from the specification of the compiler's correctness. In this setting, the compiler specification typically states that the semantics of each compiled program is bisimilar to the semantics of the original source program, i.e. both programs have the same behaviour. However, full bisimilarity for all source programs is too strong a requirement for complex source languages with unsafe behaviour for which the compiler need not make any guarantees, e.g. because programs that exhibit unsafe behaviour are ruled out by the type checker. This has long been recognised and exploited in compiler verification, but to date no calculation technique can handle such partial specifications. To address this, we propose a generalisation of bisimilarity, called skew bisimilarity, that allows us to weaken the compiler specification so that we may safely ignore unsafe behaviour when calculating a compiler for the specification. We demonstrate that skew bisimilarity enables us to derive compilers that produce more efficient code compared to previous compiler calculation techniques, all while maintaining the same strong correctness guarantees for safe source programs. We further show that -- even for source languages without unsafe behaviour -- skew bisimilarity provides a powerful generalisation of bisimilarity that enables a novel calculation technique for reasoning about register machines. This improves on existing compiler calculation techniques for register machines, which are currently limited to terminating source languages without effects. To demonstrate the effectiveness of skew bisimilarity as a proof technique for compiler calculation, we have fully formalised it in Agda and used this formalisation to calculate compilers for a variety of languages, including the first calculation of a compiler for a typed concurrent lambda calculus that targets a register machine.
@article{Bahr26,
title = {Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations},
author = {Patrick Bahr},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828683}
}