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


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

[ps file] [pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page