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.

[ps file] [pdf file]

Pointers to Related Work

A. Barber and G. Plotkin, Dual Intuitionistic Linear Logic. Submitted for publication, 1997.
J. Berdine, P.W. O'Hearn, U.S. Reddy and H. Thielecke, Linearly used continuations. In Proc. ACM SIGPLAN Workshop on Continuations (CW'01) (2001).
M. Hasegawa, Linearly used effects: monadic and CPS transformations into the linear lambda calculus. In Proc. FLOPS2002, Springer LNCS 2441 (2002).

Back to Hassei's Research Page / Home Page