Hostname: page-component-7c8c6479df-27gpq Total loading time: 0 Render date: 2024-03-27T19:09:03.684Z Has data issue: false hasContentIssue false

Computational types from a logical perspective

Published online by Cambridge University Press:  01 March 1998

P. N. BENTON
Affiliation:
Persimmon IT Inc., Cambridge, UK
G. M. BIERMAN
Affiliation:
Gonville and Caius College, Cambridge, UK
V. C. V. DE PAIVA
Affiliation:
School of Computer Science, University of Birmingham, Birmingham, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
© 1998 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.