Sciweavers

CSL
2002
Springer

Classical Linear Logic of Implications

13 years 3 months ago
Classical Linear Logic of Implications
Abstract. We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the nonlinear and linear implications as the basic constructs, and this design choice allows a technically managable axiomatization 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.
Masahito Hasegawa
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where CSL
Authors Masahito Hasegawa
Comments (0)