Cut Elimination in Multifocused Linear Logic

Taus Brock-Nannestad
(INRIA & LIX, École Polytechnique)
Nicolas Guenot
(IT University of Copenhagen)

We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule instances in focusing phases. We show that cut elimination can be performed in a sensible way even though the proof requires some specific lemmas to deal with multifocusing phases, and discuss the difficulties arising with cut elimination when considering normal forms of proofs in linear logic.

In Sandra Alves and Iliano Cervesato: Proceedings Third International Workshop on Linearity (LINEARITY 2014), Vienna, Austria, 13th July, 2014, Electronic Proceedings in Theoretical Computer Science 176, pp. 24–33.
Published: 16th February 2015.

ArXived at: https://dx.doi.org/10.4204/EPTCS.176.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org