Enriching an effect calculus with linear types

Jeff Egger; Rasmus Ejlers Møgelberg; Alex Simpson

doi:10.1007/978-3-642-04027-6_19

Enriching an effect calculus with linear types

Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson

University of Edinburgh

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

We define an ``enriched effect calculus'' by conservatively
extending a type theory for
computational effects
with primitives from linear logic. By doing so, we obtain
a generalisation of linear type theory, intended as
a formalism for expressing linear aspects of effects.

As a worked example, we formulate linearly-used continuations
in the enriched effect calculus. These are captured by a fundamental
translation of the enriched effect calculus
into itself, which extends existing call-by-value and call-by-name
linearly-used CPS translations. We show that our translation is
involutive. Full completeness results for the various linearly-used
CPS translations follow.

Our main results, the conservativity of enriching the
effect calculus with linear primitives, and the involution property
of the fundamental translation, are proved using a category-theoretic
semantics for the enriched effect calculus. In particular, the involution
property amounts to the self-duality of
the free (syntactic) model.

Original language	English
Book series	Lecture Notes in Computer Science
Volume	5771
Pages (from-to)	240
Number of pages	254
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-642-04027-6_19
Publication status	Published - 2009
Event	18th EACSL Annual Conference on Computer Science Logic - Coimbra, Portugal Duration: 7 Sept 2009 → 11 Sept 2009 Conference number: 18 http://www.mat.uc.pt/~csl/

Conference

Conference	18th EACSL Annual Conference on Computer Science Logic
Number	18
Country/Territory	Portugal
City	Coimbra
Period	07/09/2009 → 11/09/2009
Internet address	http://www.mat.uc.pt/~csl/

Keywords

- Enriched Effect Calculus
- Linear Logic
- Computational Effects
- Continuation-Passing Style (CPS) Translation
- Category-Theoretic Semantics

Access to Document

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

Modeller og detaljerede kalkuler for eﬀekter i programmeringssprog
Møgelberg, R. E. (CoI)
01/10/2007 → 31/12/2010
Project: Research

Cite this

@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.",

keywords = "- Enriched Effect Calculus, - Linear Logic, - Computational Effects, - Continuation-Passing Style (CPS) Translation, - Category-Theoretic Semantics, - Enriched Effect Calculus, - Linear Logic, - Computational Effects, - Continuation-Passing Style (CPS) Translation, - Category-Theoretic Semantics",

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/",

}

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.

KW - - Enriched Effect Calculus

KW - - Linear Logic

KW - - Computational Effects

KW - - Continuation-Passing Style (CPS) Translation

KW - - Category-Theoretic Semantics

KW - - Enriched Effect Calculus

KW - - Linear Logic

KW - - Computational Effects

KW - - Continuation-Passing Style (CPS) Translation

KW - - Category-Theoretic Semantics

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

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

M3 - Conference article

SN - 0302-9743

VL - 5771

SP - 240

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 18th EACSL Annual Conference on Computer Science Logic

Y2 - 7 September 2009 through 11 September 2009

ER -

Enriching an effect calculus with linear types

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Modeller og detaljerede kalkuler for eﬀekter i programmeringssprog

Cite this