[Prev][Next][Index][Thread]
paper announcement: Principal Typing in Elementary Affine Logic

To: "Types forum" <types@cis.upenn.edu>

Subject: paper announcement: Principal Typing in Elementary Affine Logic

From: "Paolo Coppola" <coppola@dimi.uniud.it>

Date: Tue, 29 Jan 2002 17:28:03 +0100

Importance: Normal
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/EAtyping.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 lambdacalculus EAL formulas as types. The problem is
solved by showing that very lambdaterm 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 lambdaterm, either a negative answer or the set of its
principal typing schemata.