@inproceedings{78fd27f20ddc46db848611038e764a0d,
title = "Free-cut elimination in linear logic and an application to a feasible arithmetic",
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.",
keywords = "bounded arithmetic, implicit computational complexity, linear logic, polynomial time computation, proof theory",
author = "Patrick Baillot and Anupam Das",
year = "2016",
month = aug,
day = "1",
doi = "10.4230/LIPIcs.CSL.2016.40",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl",
pages = "40:1--40:18",
editor = "Jean-Marc Talbot and Laurent Regnier",
booktitle = "25th EACSL Annual Conference on Computer Science Logic (CSL 2016)",
address = "Germany",
note = "25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic ; Conference date: 29-08-2016 Through 01-09-2016",
}