ITU

Enriching an effect calculus with linear types

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Standard

Enriching an effect calculus with linear types. / Egger, Jeff; Møgelberg, Rasmus Ejlers; Simpson, Alex.

In: Lecture Notes in Computer Science, Vol. 5771, 2009, p. 240.

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@inproceedings{5ca50da0e3ff11dea523000ea68e967b,
title = "Enriching an effect calculus with linear types",
abstract = "We define an ``enriched effect calculus'' by conservativelyextending  a type theory for computational effectswith primitives from linear logic. By doing so, we obtaina generalisation of linear type theory, intended asa formalism for expressing linear aspects of effects.As a worked example, we formulate  linearly-used continuationsin the enriched effect calculus. These are captured by a fundamentaltranslation of the enriched effect calculusinto itself, which extends existing call-by-value and call-by-namelinearly-used CPS translations. We show that our translation is involutive. Full completeness results for the various linearly-usedCPS translations  follow.Our main results, the conservativity of enriching theeffect calculus with linear primitives, and the involution propertyof the fundamental translation, are proved using a category-theoreticsemantics for the enriched effect calculus. In particular, the involutionproperty amounts to the  self-duality ofthe free (syntactic) model.",
author = "Jeff Egger and M{\o}gelberg, {Rasmus Ejlers} and Alex Simpson",
note = "Volume: 5771/2009; 18th EACSL Annual Conference on Computer Science Logic, CSL 09 ; Conference date: 07-09-2009 Through 11-09-2009",
year = "2009",
doi = "10.1007/978-3-642-04027-6_19",
language = "English",
volume = "5771",
pages = "240",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",
url = "http://www.mat.uc.pt/~csl/",

}

RIS

TY - GEN

T1 - Enriching an effect calculus with linear types

AU - Egger, Jeff

AU - Møgelberg, Rasmus Ejlers

AU - Simpson, Alex

N1 - Conference code: 18

PY - 2009

Y1 - 2009

N2 - We define an ``enriched effect calculus'' by conservativelyextending  a type theory for computational effectswith primitives from linear logic. By doing so, we obtaina generalisation of linear type theory, intended asa formalism for expressing linear aspects of effects.As a worked example, we formulate  linearly-used continuationsin the enriched effect calculus. These are captured by a fundamentaltranslation of the enriched effect calculusinto itself, which extends existing call-by-value and call-by-namelinearly-used CPS translations. We show that our translation is involutive. Full completeness results for the various linearly-usedCPS translations  follow.Our main results, the conservativity of enriching theeffect calculus with linear primitives, and the involution propertyof the fundamental translation, are proved using a category-theoreticsemantics for the enriched effect calculus. In particular, the involutionproperty amounts to the  self-duality ofthe free (syntactic) model.

AB - We define an ``enriched effect calculus'' by conservativelyextending  a type theory for computational effectswith primitives from linear logic. By doing so, we obtaina generalisation of linear type theory, intended asa formalism for expressing linear aspects of effects.As a worked example, we formulate  linearly-used continuationsin the enriched effect calculus. These are captured by a fundamentaltranslation of the enriched effect calculusinto itself, which extends existing call-by-value and call-by-namelinearly-used CPS translations. We show that our translation is involutive. Full completeness results for the various linearly-usedCPS translations  follow.Our main results, the conservativity of enriching theeffect calculus with linear primitives, and the involution propertyof the fundamental translation, are proved using a category-theoreticsemantics for the enriched effect calculus. In particular, the involutionproperty amounts to the  self-duality ofthe free (syntactic) model.

U2 - 10.1007/978-3-642-04027-6_19

DO - 10.1007/978-3-642-04027-6_19

M3 - Conference article

VL - 5771

SP - 240

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

T2 - 18th EACSL Annual Conference on Computer Science Logic

Y2 - 7 September 2009 through 11 September 2009

ER -

ID: 1037207