Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.40
URN: urn:nbn:de:0030-drops-65807
URL: https://drops.dagstuhl.de/opus/volltexte/2016/6580/
Baillot, Patrick ; Das, Anupam
Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic
| pdf-format: |
|
Abstract
We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.
BibTeX - Entry
@InProceedings{baillot_et_al:LIPIcs:2016:6580,
author = {Patrick Baillot and Anupam Das},
title = {{Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {40:1--40:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Jean-Marc Talbot and Laurent Regnier},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6580},
URN = {urn:nbn:de:0030-drops-65807},
doi = {10.4230/LIPIcs.CSL.2016.40},
annote = {Keywords: proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity}
}
| Keywords: | proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity | |
| Seminar: | 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 29.08.2016 |
