1998/03/01 by P. N. Benton, Gavin Bierman, Valeria de Paiva · 2 citations
Computer Science · Mathematics · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic #Curry–Howard correspondence #Natural deduction #Cartesian closed category #Sequent calculus #Computer science #Calculus (dental) #Monad (category theory) #Lambda calculus #Intuitionistic logic #Typed lambda calculus #Confluence #Propositional calculus #Algebra over a field #Simply typed lambda calculus #Linear logic #Church encoding #Mathematics #Discrete mathematics #Programming language #Pure mathematics #Theoretical computer science
paper · pdf · doi:10.1017/s0956796898002998
openalex publication_date 1998/03/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/04
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.