License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.39
URN: urn:nbn:de:0030-drops-40515
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4051/
Go to the corresponding LIPIcs Volume Portal

Accattoli, Beniamino

Linear Logic and Strong Normalization

pdf-format:
4.pdf (0.6 MB)

Abstract

Strong normalization for linear logic requires elaborated rewriting techniques. In this paper we give a new presentation of MELL proof nets, without any commutative cut-elimination rule. We show how this feature induces a compact and simple proof of strong normalization, via reducibility candidates. It is the first proof of strong normalization for MELL which does not rely on any form of confluence, and so it smoothly scales up to full linear logic. Moreover, it is an axiomatic proof, as more generally it holds for every set of rewriting rules satisfying three very natural requirements with respect to substitution, commutation with promotion, full composition, and Kesner's IE property. The insight indeed comes from the theory of explicit substitutions, and from looking at the exponentials as a substitution device.

BibTeX - Entry

@InProceedings{accattoli:LIPIcs:2013:4051,
  author =	{Beniamino Accattoli},
  title =	{{Linear Logic and Strong Normalization}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{39--54},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4051},
  URN =		{urn:nbn:de:0030-drops-40515},
  doi =		{10.4230/LIPIcs.RTA.2013.39},
  annote =	{Keywords: linear logic, proof nets, strong normalization, explicit substitutions}
}

Keywords: linear logic, proof nets, strong normalization, explicit substitutions
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI