TY - JOUR
T1 - Models for the computational λ-calculus
AU - Power, John
PY - 2001
Y1 - 2001
N2 - We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first consider the class of closed -categories, a natural and direct generalisation of the notion of cartesian closed category. We then consider closed ·-categories, which are based upon indexed categories and which are closely related to modern compiling technology. Finally, we consider the class of cartesian closed categories · together with a ·-enriched monad. The latter class has the most developed abstract theory, which one can adopt and by which one can dispense with coherence details in the spirit of Mac Lane involving strengths.
AB - We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first consider the class of closed -categories, a natural and direct generalisation of the notion of cartesian closed category. We then consider closed ·-categories, which are based upon indexed categories and which are closely related to modern compiling technology. Finally, we consider the class of cartesian closed categories · together with a ·-enriched monad. The latter class has the most developed abstract theory, which one can adopt and by which one can dispense with coherence details in the spirit of Mac Lane involving strengths.
UR - http://dx.doi.org/10.1016/S1571-0661(05)80056-8
U2 - 10.1016/S1571-0661(05)80056-8
DO - 10.1016/S1571-0661(05)80056-8
M3 - Article
SN - 1571-0661
VL - 40
SP - 288
EP - 301
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -