The enriched effect calculus: syntax and semantics
The enriched effect calculus: syntax and semantics
复制标题
丰富的效果演算：语法和语义
DOI：
10.1093/logcom/exs025
复制
发表时间：
2012
影响因子：
0.7
通讯作者：
Egger J
中科院分区：
文献类型：
--
作者：
Egger J
本文介绍了丰富的效果演算，它扩展了已建立的类型理论的计算效果与原语从线性逻辑。新演算提供了一种表示计算效果的线性方面的形式，例如状态和/或延续等命令性特征的线性使用，丰富的效果演算是作为没有线性原语的基本效果演算的扩展来实现的，它与Moggi的计算元语言、Filinski的效果PCF和Levy的按推值调用密切相关。我们提出的句法结果表明：的保真度的线性连接词的行为丰富的效果演算;保守性的丰富的效果演算在其非线性核心（效果演算）;以及直觉线性逻辑作为丰富效应演算的扩展时的非保守性。文章的后半部分研究了丰富效应演算的模型，基于丰富范畴理论。我们给出了几个这样的模型的例子，将它们与标准效应演算模型（如基于单子的模型）和直觉线性逻辑模型联系起来。我们还证明了可靠性和完备性。
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.
登录
查看更多内容
按值调用模型中的线性使用状态
DOI：
10.1007/978-3-642-22944-2_21
发表时间：
2011
期刊：
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
R. E. Møgelberg;S. Staton
通讯作者：
S. Staton
DOI：
--
发表时间：
2004
期刊：
Workshop on Domains
影响因子：
--
作者：
Gordon D. Plotkin;John Power
通讯作者：
John Power
影响因子：
0.6
作者：
J. Laird
通讯作者：
J. Laird
代数范畴中的余均衡器
影响因子：
0.5
作者：
F. E. J. Linton
通讯作者：
F. E. J. Linton
计算类型的可归约性和 TT-Lifting
DOI：
10.1007/11417170_20
发表时间：
2005
期刊：
ACM SIGLOG News
影响因子：
--
作者：
S. Lindley;Ian Stark
通讯作者：
Ian Stark