Light linear logics

Light linear logics are variants of linear logic characterizing complexity classes. They are designed by defining alternative exponential connectives, which induce a complexity bound on the cut-elimination procedure.

Light linear logics are one of the approaches used in \textit{implicit computational complexity},  the research area studying the computational complexity of programs without referring to external measuring conditions or particular machine models. 

\section{Elementary linear logic} \section{Light linear logic}