ITU

Enriching an effect calculus with linear types

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

View graph of relations

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 languageEnglish
Book seriesLecture Notes in Computer Science
Volume5771
Pages (from-to)240
Number of pages254
ISSN0302-9743
DOIs
Publication statusPublished - 2009
Event18th EACSL Annual Conference on Computer Science Logic - Coimbra, Portugal
Duration: 7 Sep 200911 Sep 2009
Conference number: 18
http://www.mat.uc.pt/~csl/

Conference

Conference18th EACSL Annual Conference on Computer Science Logic
Number18
CountryPortugal
CityCoimbra
Period07/09/200911/09/2009
Internet address

ID: 1037207