[Prev][Next][Index][Thread]

paper announcement: Principal Typing in Elementary Affine Logic

I am pleased to announce the paper "Principal Typing in Elementary Affine
Logic" by P. Coppola and S. Ronchi Della Rocca, available at:

http://www.dimi.uniud.it/~coppola/papers/EA-typing.pdf

Best regards,
Paolo Coppola

*****************************************************************
Abstract

Elementary Affine Logic (EAL) is a variant of the Linear Logic
characterizing the computational power of the elementary bounded Turing
machines. The EAL Type Inference problem is the problem of automatically
assign to terms of lambda-calculus EAL formulas as types. The problem is
solved by showing that very lambda-term which is typeable has a finite set
of principal typing schemata, from which all and only its typings can be
derived, through suitable operations. An algorithm is showed, that gives as
output, for every lambda-term, either a negative answer or the set of its
principal typing schemata.