Principal Typing for Lambda Calculus in Elementary Affine Logic.

ElementaryAffineLogic(EAL)isavariantofLinearLogiccharacterizingthecomputa- tional power of the elementary bounded Turing machines. The EAL Type Inference problem is the problem of automatically assigning to terms of -calculus EAL formulas as types. This problem, re- stricted to the propositional fragment of EAL, is proved to be decidable, and an algorithm is shown, building, for every -term, either a negative answer or a finite set of type schemata, from which all and only its typings can be derived, through suitable operations.