Enriching an effect calculus with linear types

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.