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: https://drops.dagstuhl.de/opus/volltexte/2013/4051/
Accattoli, Beniamino
Linear Logic and Strong Normalization
| pdf-format: |
|
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 | |
| Seminar: | 24th International Conference on Rewriting Techniques and Applications (RTA 2013) | |
| Issue date: | 2013 | |
| Date of publication: | 24.06.2013 |
