Modal and fixpoint linear logic.

Abstract

This thesis provides adaptations of the algebraic and relational semantics of modal logic to model J.-Y. Girard's linear logic extended with general modalities. This work extends the work of M. D'Agostino, D. Gabbay, and A. Russo on modalities in implication systems, which include a fragment of linear logic, and the work of J.-Y. Girard on phase semantics for linear logic. We develop deductive systems based on the Gentzen-style sequent calculi of Ohnishi and Matsumoto and the indexed sequents of Mints, and prove cut-elimination properties. We show that semantics and deductive systems that are equivalent for classical modal logic become nonequivalent when adapted to linear logic. We also provide a semantics based on Girard's phase semantics for the fixpoint operators of the modal mu-calculus, developed by D. Kozen, E. A. Emerson, E. Clarke, and others, in linear logic, and consider the translation of Y. Lafont's exponentials with the Free Storage rule into linear logic with fixpoint operators.