Parameterizations and fixed-point operators on control categories

Yoshihiko Kakutani and Masahito Hasegawa

In Proc. 6th International Conference on Typed Lambda Calculi and Applications (TLCA'03), Springer LNCS 2701 (2003) pages 180-194


The \lambda\mu-calculus features both variables and names, together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a bi-parameterized family of operators. In this paper, we study these bi-parameterized operators on Selinger's categorical models of the \lambda\mu-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important case, we study parameterizations of uniform fixed-point operators on control categories, and show bijective correspondences between parameterized fixed-point operators and non-parameterized ones under uniformity conditions.

© Springer-Verlag 2003

[pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page