Linear-use CPS translations in the enriched effect calculus

DOI10.2168/LMCS-8(4:2)2012zbMATH Open1273.03164arXiv1209.4268OpenAlexW2014379452MaRDI QIDQ3166223FDOQ3166223

Authors: J. M. Egger, Rasmus Ejlers Møgelberg, Alex Simpson 

Publication date: 22 October 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: The enriched effect calculus (EEC) is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. This paper explores the enriched effect calculus as a target language for continuation-passing-style (CPS) translations in which the typing of the translations enforces the linear usage of continuations. We first observe that established call-by-value and call-by name linear-use CPS translations of simply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the fragment of ILL given by EEC. These two translations are uniformly generalised by a single generic translation of the enriched effect calculus into itself. As our main theorem, we prove that the generic self-translation of EEC is involutive up to isomorphism. As corollaries, we obtain full completeness results, both for the generic translation, and for the original call-by-value and call-by-name translations.

Full work available at URL: https://arxiv.org/abs/1209.4268

Recommendations

• Linearly-Used Continuations in the Enriched Effect Calculus
• Enriching an Effect Calculus with Linear Types
• The enriched effect calculus: syntax and semantics
• scientific article; zbMATH DE number 1942458
• Linear usage of state

zbMATH Keywords

linear logiccomputational metalanguagecontinuation-passing-style translationeffect calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30)

Cited In (5)

• CPS-translation as adjoint
• Classical control and quantum circuits in enriched category theory
• Linearly-Used Continuations in the Enriched Effect Calculus
• Enriching an Effect Calculus with Linear Types
• Title not available (Why is that?)

This page was built for publication: Linear-use CPS translations in the enriched effect calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3166223)