Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)
复制标题
在语义课程中通过混合嵌入跳过活页夹官僚机构（功能性珍珠）
DOI：
10.1145/3473599
复制
发表时间：
2021
影响因子：
--
通讯作者：
A. Chlipala
中科院分区：
文献类型：
--
作者：
A. Chlipala
关于程序的严格推理要求在管理变量绑定等细节方面有一定程度的官僚主义，但是，在引导学生了解语义上的大思想时，我们可能希望将开销最小化。我们描述了我们的实验，引入了一系列这样的想法，使用Coq证明助手，没有任何显式的变量表示，而是使用我们称之为“混合嵌入”的高阶语法编码：它既不是深度嵌入的完全显式语法，也不是浅嵌入的无语法编程。Marquee示例包括对并发推理的不同理解，包括传统的模型检查（部分阶约简）、程序逻辑（并发分离逻辑）和类型检查（会话类型）——所有这些都在变量上没有任何附带条件。
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.