一句话：提出程序副词及 Tlön 嵌入，为带效应语言提供比自由单子更灵活且保留更多语法结构的形式语义。
自由单子及其变体已成为在证明助手中表示带效应程序语义的通用工具，但它们并非组织效应计算的唯一方式。受 applicative functor、selective functor 等结构启发，本文定义了一组称为“程序副词”（program adverbs）的数据结构与理论，用以刻画多种计算模式；这些程序副词自身可组合，因而能描述具有多种计算模式的语言语义。作者进一步以程序副词为基础提出一类新的语义嵌入，称为 Tlön 嵌入。与基于自由单子的嵌入相比，Tlön 嵌入在效应计算建模上更灵活，同时保留更多关于程序语法结构的信息。
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ön embeddings. Compared with embeddings based on free monads, Tlön embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.