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

VL - 40

SP - 288

EP - 301

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -