Control categories and duality: On the categorical semantics of the lambda-mu calculus (Q2719799)

Advantages and disadvantages of the two parameter passing techniques, call-by-value and call-by-name, have been debated for a long time. NEWLINENEWLINENEWLINEIn the present paper the author gives a categorical semantics to the call-by-name and call-by-value versions of Parigot's \(\lambda\mu\) calculus with disjunction types. He introduces the class of control categories and proves, via a categorical structure theorem, that the categorical semantics is equivalent to a continuation passing style (CPS) semantics in the style of Hofmann and Streicher. He shows 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 co-control categories. As a corollary he obtains 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.