Technical reports
Computational types from a logical perspective I
P.N. Benton, G.M. Bierman, V.C.V. de Paiva
May 1995, 19 pages
DOI: 10.48456/tr-365
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 a strong normalisation result.
Full text
PDF (1.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-365, author = {Benton, P.N. and Bierman, G.M. and de Paiva, V.C.V.}, title = {{Computational types from a logical perspective I}}, year = 1995, month = may, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-365.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-365}, number = {UCAM-CL-TR-365} }