Principal typing for lambda calculus in elementary affine logic : dart-reports : Cop+Ron:FI-2005

P. Coppola and Simona Ronchi Della Rocca

Principal typing for lambda calculus in elementary affine logic

Fundamenta Informaticae, 65(1-2):87-112, 2005

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 l-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 l-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 | .pdf ]

Back

This file has been generated by bibtex2html 1.43