P. N. BENTON a1, G. M. BIERMAN a2andV. 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
Abstract
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.
