Paolo Coppola and Simona Ronchi Della Rocca. Principal typing for elementary affine logic. In Hofmann M., editor, Typed Lambda Calculi and Applications: 6th International Conference (TLCA 2003), volume 2701 of Lecture Notes in Computer Science, pages 90-104, Berlin, 2003. Springer-Verlag. A preliminary version has been presented at the workshop ``LL-Linear Logic'', affiliated to FLoC'02, Copenhagen.

Elementary Affine Logic (EAL) is a variant of the Linear Logic characterizing the computational power of the elementary bounded Touring machines. The EAL Type Inference problem is the problem of automatically assign to terms of lambda-calculus EAL formulas as types. This problem is proved to be decidable, and an algorithm is showed, building, for every lambda-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.

[ bib | http | .pdf ]

Back