Enriching an effect calculus with linear types

Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson

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


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
Pages (from-to)240
Number of pages254
Publication statusPublished - 2009
Event18th EACSL Annual Conference on Computer Science Logic - Coimbra, Portugal
Duration: 7 Sept 200911 Sept 2009
Conference number: 18


Conference18th EACSL Annual Conference on Computer Science Logic
Internet address


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


Dive into the research topics of 'Enriching an effect calculus with linear types'. Together they form a unique fingerprint.

Cite this