Dear Category Theorists, 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. Let me briefly summarize the part of the paper that I think will be the most interesting to category theorists; the actual abstract is appended at the end. Consider a category C with distributive finite products and coproducts and a distinguished object R, such that all exponentials of the form R^A exist. Let R^C denote the full subcategory of C consisting of objects of the form R^A. It is an old observation that R^C is cartesian-closed. This observation is at the heart of continuation passing style (CPS) interpretations of programming languages with control operators, and it has been used recently by Hofmann and Streicher to give a sound and complete categorical model of Parigot's lambda-mu calculus. (The lambda-mu calculus generalizes the simply-typed lambda calculus; it is a proof term calculus for propositional classical logic). In this paper, I give an independent, algebraic characterization of the structure of categories of the form R^C. By "independent", I mean that it does not depend on an ambient category C, and by "algebraic", that it is given in terms of operations and equations only. The crucial structure that R^C has, besides cartesian closure, is an operation called "classical disjunction" that takes R^A and R^B to R^(AxB). This operation is functorial in each argument, but not bifunctorial; it forms a premonoidal structure in the sense of Power and Robinson. Abstracting from R^C, I define the class of "control categories", which are cartesian-closed categories with a premonoidal structure and suitable axioms. The presence of an operation which is not bifunctorial leads to some interesting twists, as one has to be a bit careful about how one defines concepts such as weak structure-preserving functors and equivalences of categories. The main theorem is a structure theorem, which shows that every control category is equivalent to a category of the form R^C (and, of course, vice versa). An algebraic class of categories calls out for an internal language. I prove that the call-by-name lambda-mu calculus (with product and disjunction types) forms an internal language for control categories. Thus, these categories can be considered as models for (a certain kind of) proof theory of classical logic. Also, the call-by-value lambda-mu-calculus forms an internal language for the dual class of co-control categories. As a consequence of this categorical duality, it follows that there is a syntactic duality between the call-by-name and the call-by-value calculus, i.e., there are mutually inverse translations between call-by-name and call-by-value that preserve the categorical (and also the operational) semantics. Such dualities have been observed in a different setting by Filinski. In the case of the lambda-mu calculus, such a syntactic duality was conjectured by Streicher and Reus. 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.