Affiliations: Dipartimento di Matematica e Informatica –
Università di Udine, via delle Scienze 206, I-33100 Udine, Italy.
coppola@dimi.uniud.it | Dipartimento di Informatica – Università di
Torino, Corso Svizzera 185, I-10149 Torino, Italy. ronchi@di.unito.it
Note: [] Address for correspondence: Dipartimento di Matematica e
Informatica - Università di Udine, via delle Scienze 206, I-33100 Udine,
Italy
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.
