一句话：提出混合嵌入的高阶语法编码，在 Coq 语义课程中无需显式变量，消除绑定细节的证明负担。
论文报告在语义课程中引入 Coq 教学实验：传统上严格推理程序需要显式管理变量绑定，带来大量“绑定器官僚主义”开销。作者提出“混合嵌入”编码，它既不是完全显式的 deep embedding，也不是无语法约束的 shallow embedding，而是在高阶语法中省去变量表示。课程以此讲解并发推理的多种传统：模型检测中的偏序归约、程序逻辑中的并发分离逻辑，以及类型检查中的会话类型，全部无需变量侧条件。该函数式珍珠表明，学生可以在避免绑定细节负担的同时接触语义学核心思想。
Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.
@article{paperbot1108,
title = {Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)},
author = {Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473599}
}