@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",

}