Models for the computational λ-calculus

John Power

Research output: Contribution to journalArticlepeer-review

9 Citations (SciVal)


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.
Original languageEnglish
Pages (from-to)288-301
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2001


Dive into the research topics of 'Models for the computational λ-calculus'. Together they form a unique fingerprint.

Cite this