• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >The enriched effect calculus: syntax and semantics
【24h】

The enriched effect calculus: syntax and semantics

机译：丰富的效果演算：语法和语义

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This article introduces the enriched effect calculus, which extends established type theories for computational effects with primitives from linear logic. The new calculus provides a formalism for expressing linear aspects of computational effects; e.g. the linear usage of imperative features such as state and/or continuations. The enriched effect calculus is implemented as an extension of a basic effect calculus without linear primitives, which is closely related to Moggi's computational metalanguage, Filinski's effect PCF and Levy's call-by-push-value. We present syntactic results showing: the fidelity of the behaviour of the linear connectives of the enriched effect calculus; the conservativity of the enriched effect calculus over its non-linear core (the effect calculus); and the non-conservativity of intuitionistic linear logic when considered as an extension of the enriched effect calculus. The second half of the article investigates models for the enriched effect calculus, based on enriched category theory. We give several examples of such models, relating them to models of standard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.
机译：本文介绍了丰富的效果演算，它利用线性逻辑中的图元扩展了用于计算效果的既定类型理论。新的演算为表达计算效果的线性方面提供了形式主义。例如命令性要素（例如状态和/或延续）的线性用法。丰富的效果演算是对没有线性图元的基本效果演算的扩展，它与Moggi的计算元语言，Filinski的效果PCF和Levy的按推调用值密切相关。我们给出的句法结果表明：富集效应演算的线性连接词行为的保真度；丰富的效应演算在其非线性核心上的保守性（效应演算）；直觉线性逻辑的非保守性被视为丰富效应演算的扩展。本文的下半部分基于丰富类别理论研究了丰富效果演算的模型。我们给出了此类模型的几个示例，将它们与标准效果计算的模型（例如基于单子的计算）和直觉线性逻辑模型相关联。我们还证明了完整性和完整性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号