Enriching an effect calculus with linear types

Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

Abstrakt

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.


OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind5771
Sider (fra-til)240
Antal sider254
ISSN0302-9743
DOI
StatusUdgivet - 2009
BegivenhedComputer Science Logic - Coimbra, Portugal
Varighed: 7 sep. 200911 sep. 2009
Konferencens nummer: 18
http://www.mat.uc.pt/~csl/

Konference

KonferenceComputer Science Logic
Nummer18
Land/OmrådePortugal
ByCoimbra
Periode07/09/200911/09/2009
Internetadresse

Fingeraftryk

Dyk ned i forskningsemnerne om 'Enriching an effect calculus with linear types'. Sammen danner de et unikt fingeraftryk.

Citationsformater