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

    We show that Buss' witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based in linear logic, by taking advantage of free-cut elimination. The De Morgan normal form available in classical (linear) logic means that the functions we extract remain at ground type, based on the usual safe recursive programs of \cite{BelHof:02}. A similar proof method was used by Cantini in \cite{Cantini02}, who uses combinatory terms as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}

%    We illustrate in the same time the relationship between  $\mathcal{A}_2^1$ and linear logic, which was hinted but not investigated in the original paper  \cite{BelHof:02}.  

We conclude in Sect.~\ref{sect:conclusions} with a survey of related work and some avenues for further applications of the free-cut elimination result.