Program adverbs and Tlön embeddings
Program adverbs and Tlön embeddings
复制标题
程序副词和 Tlön 嵌入
DOI：
10.1145/3547632
复制
发表时间：
2022
影响因子：
--
通讯作者：
Weirich, Stephanie
中科院分区：
文献类型：
--
作者：
Li, Yao;Weirich, Stephanie
自由单子（及其变体）已经成为一种流行的通用工具，用于在证明助手中表示有效程序的语义。这些数据结构支持由未解释事件参数化的语义的组合定义，同时承认丰富的等价等价理论。但是单子并不是构造有效计算的唯一方法，我们为什么要限制自己呢？在本文中，受应用函子、选择函子和其他结构的启发，我们定义了一组数据结构和理论，我们称之为程序副词，它们捕获了各种计算模式。程序副词本身是可组合的，允许它们用于指定具有多种计算模式的语言的语义。我们使用程序副词作为一类新的语义嵌入的基础，这种语义嵌入被称为Tl\ \ on嵌入。与基于自由单体的嵌入相比，Tl\ \ on嵌入在效果的计算建模方面具有更大的灵活性，同时保留了有关程序语法结构的更多信息。
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves? In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tl\"on embeddings. Compared with embeddings based on free monads, Tl\"on embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.
登录
查看更多内容
在语义课程中通过混合嵌入跳过活页夹官僚机构（功能性珍珠）
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
重新加载方程：Coq 中的高级依赖类型函数编程和证明
影响因子：
--
作者：
Matthieu Sozeau;Cyprien Mangin
通讯作者：
Cyprien Mangin
更深浅的嵌入
DOI：
--
发表时间：
2022
期刊：
International Conference on Interactive Theorem Proving
影响因子：
--
作者：
Prinz, Jacob;Kavvos, G. A.;Lampropoulos, Leonidas
通讯作者：
Lampropoulos, Leonidas
共归纳恢复单子
DOI：
10.1016/j.entcs.2014.10.015
发表时间：
2014
影响因子：
0.7
作者：
Maciej Piróg;J. Gibbons
通讯作者：
J. Gibbons
影响因子：
0.6
作者：
Capretta, Venanzio
通讯作者：
Capretta, Venanzio