Classical linear logic of implications
Conference of the European Association for Computer Science Logic
2471 (2002) pages 458-472
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 non-linear 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.
© Springer-Verlag 2002
Pointers to Related Work
Back to Hassei's
Research Page / Home Page