Control categories and duality: on the categorical semantics of the lambda-mu calculus
Control categories and duality: on the categorical semantics of the lambda-mu calculus
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 …