Light Logics and Optimal Reduction: Completeness and Complexity

Patrick Baillot, Paolo Coppola, Ugo Dal Lago

Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL, resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (E…