Abstract
Elementary Affine Logic (EAL) is a variant of Linear Logic characterizing the computational 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, restricted 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.
Get full access to this article
View all access options for this article.