[Prev][Next][Index][Thread]
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
http://www.math.lsa.umich.edu/~selinger/papers.html
http://hypatia.dcs.qmw.ac.uk/author/SelingerP
This is a revised and improved version of a paper I presented at
MFPS'98. Comments are welcome.
Best wishes, -- Peter Selinger
----------------------------------------------------------------------
ABSTRACT:
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.