Article contents
Classical linear logic of implications
Published online by Cambridge University Press: 14 March 2005
Abstract
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
- Information
- Copyright
- 2005 Cambridge University Press
- 6
- Cited by