Journal of Functional Programming

Computational types from a logical perspective

P. N. BENTON a1, G. M. BIERMAN a2 and V. C. V. DE PAIVA a3
a1 Persimmon IT Inc., Cambridge, UK
a2 Gonville and Caius College, Cambridge, UK
a3 School of Computer Science, University of Birmingham, Birmingham, UK


Moggi's computational lambda calculus is a metalanguage for denotational semantics which arose from the observation that many different notions of computation have the categorical structure of a strong monad on a cartesian closed category. In this paper we show that the computational lambda calculus also arises naturally as the term calculus corresponding (by the Curry–Howard correspondence) to a novel intuitionistic modal propositional logic. We give natural deduction, sequent calculus and Hilbert-style presentations of this logic and prove strong normalisation and confluence results.