### Classical linear logic of implications

Masahito Hasegawa
In
*Proc. Annual
Conference of the European Association for Computer Science Logic
(CSL'02)*,
Springer LNCS
2471 (2002) pages 458-472

### 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 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