## 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.

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 | |

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 |

## Keywords

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