类型和效果系统语义学中逻辑关系的因子分解系统和一元提升
Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
摘要：
类型和效果系统包含有关计算效果的信息，例如，状态变化、概率选择或I/O，程序短语可以在其返回值旁边调用。类型和效果系统的语义涉及一个参数化的单子族，其大小与效果的数量成指数关系。我们从类别上的单个单子、该单子的代数运算选择以及该类别上合适的因子分解系统中推导出如此精确的语义。我们使用纤维化的逻辑关系的原始语义派生的语义。我们的证明使用了一种民间传说中的技术来提升单子的操作。
英文摘要：
Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
