Hostname: page-component-6bf8c574d5-2jptb Total loading time: 0 Render date: 2025-02-21T05:57:11.097Z Has data issue: false hasContentIssue false

Classical linear logic of implications

Published online by Cambridge University Press:  14 March 2005

MASAHITO HASEGAWA
Affiliation:
Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502 Japan PRESTO, Japan Science and Technology Agency Email: hassei@kurims.kyoto-u.ac.jp
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.

We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's dual-context system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically manageable axiomatisation without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads.

Type
Paper
Copyright
2005 Cambridge University Press