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

}

\section{Introduction and motivation}

Today, there are countless approaches towards characterising complexity classes via logic.

Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory.

To some extent there is a distinction between various notions of `representability', namely between logics that type terms computing functions of a given complexity class, and theories that prove the totality of functions in a given complexity class.

Perhaps a more important (and somewhat orthogonal) distinction for the \textsc{Dice-Fopara} community is whether the constraints on the logic or theory are \emph{implicit} or \emph{explicit}. The former includes constraints such as ramification, type level and substructural considerations, while the latter includes bounded quantification, bounded modalities (e.g. in bounded linear logic) etc. This distinction is also naturally exhibited in associated function algebras, e.g. Cobham vs. Bellantoni-Cook \cite{Cobham,BellantoniCook92}.