Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

%\documentclass[a4paper]{article}

\documentclass[a4paper,UKenglish]{lipics-v2016}

%This is a template for producing LIPIcs articles.

%See lipics-manual.pdf for further information.

%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"

%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"

% for section-numbered lemmas etc., use "numberwithinsect"

\usepackage{microtype}%if unwanted, comment out or use option "draft"

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

\bibliographystyle{plainurl}% the recommended bibstyle

\usepackage[lutzsyntax]{virginialake}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{amsthm}

\usepackage{times}

%\usepackage{sans}

\usepackage{cmll}

\usepackage{bm}

\input{macros}

\begin{document}

% Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Free-cut elimination in linear logic and an application to a feasible arithmetic\footnote{

This work was supported by by the ANR Project ELICA ANR-14-CE25-0005 and by the LABEX MILYON (ANR-10-LABX-0070) of Universit\'e de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-

0007) operated by the French National Research Agency (ANR).}

}

%\titlerunning{A Sample LIPIcs Article} %optional, in case that the title is too long; the running title should fit into the top page column

%% Please provide for each author the \author and \affil macro, even when authors have the same affiliation, i.e. for each author there needs to be the  \author and \affil macros

\author{Patrick Baillot}

\author{Anupam Das}

\affil{Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP

%	\\

%	\texttt{open@dummyuniversity.org}

	}

%\affil[1]{Dummy University Computing Laboratory, Address/City, Country\\

%  \texttt{open@dummyuniversity.org}}

%\affil[2]{Department of Informatics, Dummy College, Address/City, Country\\

%  \texttt{access@dummycollege.org}}

\authorrunning{P.\ Baillot and A.\ Das} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et. al.'

\Copyright{Patrick Baillot and Anupam Das}%mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\subjclass{F.4.1 Mathematical Logic.}

%Dummy classification -- please refer to \url{http://www.acm.org/about/class/ccs98-html}}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation".

\keywords{proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity}

%\keywords{Dummy keyword -- please provide 1--5 keywords}% mandatory: Please provide 1-5 keywords

%% Author macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\EventEditors{John Q. Open and Joan R. Acces}

%\EventNoEds{2}

%\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}

%\EventShortTitle{CVIT 2016}

%\EventAcronym{CVIT}

%\EventYear{2016}

%\EventDate{December 24--27, 2016}

%\EventLocation{Little Whinging, United Kingdom}

%\EventLogo{}

%\SeriesVolume{42}

%\ArticleNo{23}

% Editor-only macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\maketitle

\begin{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.

%We conclude with some comments for further applications of the free-cut elimination result.

 \end{abstract}

\input{introduction}

\input{preliminaries}

\input{free-cut-elim}

\input{arithmetic}

\input{bc}

\input{bc-convergence}

\input{wfm}

\input{further-work}

\input{conclusions}

\bibliographystyle{plain}

\bibliography{biblio}

\newpage

\input{appendix}

\end{document}