Paper Announcement: Control Categories and Duality

The paper "Control Categories and Duality: on the Categorical
Semantics of the Lambda-Mu Calculus" is now available from


This is a revised and improved version of a paper I presented at
MFPS'98. Comments are welcome.

Best wishes, -- Peter Selinger



We give a categorical semantics to the call-by-name and call-by-value
versions of Parigot's lambda-mu 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
lambda-mu calculus forms an internal language for control categories,
and that the call-by-value lambda-mu 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 which are mutually inverse and which
preserve the operational semantics.  This answers a question of
Streicher and Reus.