Abstract

Recently, Thielecke has introduced tensor-not categories as categorical models for functional languages in the presence of control operators. In this talk, I will introduce the closely related class of "control categories". I will show that Parigot's call-by-name lambda mu calculus, when extended with products and sum types, forms an internal language for these categories. Moreover, the call-by-value lambda mu calculus forms an internal language for the dual co-control categories. As a consequence, one obtains a syntactic, isomorphic translation between call-by-name and call-by-value which preserves the operational semantics, answering a question of Streicher and Reus. Thus, in this setting one can make precise the duality between demand-driven and value-driven computation.