Department of Computer Science and Technology

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}
}