Hostname: page-component-76fb5796d-vvkck Total loading time: 0 Render date: 2024-04-27T03:52:05.686Z Has data issue: false hasContentIssue false

Control categories and duality: on the categorical semantics of the lambda-mu calculus

Published online by Cambridge University Press:  30 March 2001

PETER SELINGER
Affiliation:
Department of Mathematics, University of Michigan, Ann Arbor, MI 48109-1109, U.S.A. Email: selinger@umich.edu

Abstract

We give a categorical semantics to the call-by-name and call-by-value versions of Parigot's λμ-calculus with disjunction types. We introduce the class of control categories, which combine a cartesian-closed structure with a premonoidal structure in the sense of Power and Robinson. We prove, via a categorical structure theorem, that the categorical semantics is equivalent to a CPS semantics in the style of Hofmann and Streicher. We show that the call-by-name λμ-calculus forms an internal language for control categories, and that the call-by-value λμ-calculus forms an internal language for the dual co-control categories. As a corollary, we obtain a syntactic duality result: there exist syntactic translations between call-by-name and call-by-value that are mutually inverse and preserve the operational semantics. This answers a question of Streicher and Reus.

Type
Research Article
Copyright
2001 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)