Computational Types from a Logical Perspective Export

@article{citeulike:401351, 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...}, author = {Benton, P. N. and Bierman, Gavin and de Paiva, Valeria}, citeulike-article-id = {401351}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.2029}, journal = {Journal of Functional Programming}, keywords = {logic, modal, own}, number = {2}, pages = {177--193}, posted-at = {2005-11-19 16:43:18}, priority = {0}, title = {Computational Types from a Logical Perspective}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.2029}, volume = {8}, year = {1998} }

TY - JOUR ID - citeulike:401351 L3 - citeulike-article-id:401351 N2 - 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... IS - 2 JF - Journal of Functional Programming EP - 193 TI - Computational Types from a Logical Perspective VL - 8 SP - 177 KW - logic KW - modal KW - own AU - Benton, PN AU - Bierman, Gavin AU - de Paiva, Valeria PY - 1998/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.2029 ER -