[Prev][Next][Index][Thread]
new paper on type inference in light logic

To: types@cis.upenn.edu

Subject: new paper on type inference in light logic

From: Patrick Baillot <pb@lipn.univparis13.fr>

Date: Thu, 13 Feb 2003 12:50:22 +0100

UserAgent: Internet Messaging Program (IMP) 3.0
I would like to announce the availability of the following paper at:
http://wwwlipn.univparis13.fr/~baillot/Publications/publications.html
Your comments and suggestions are welcome,
Patrick Baillot

Type inference for polynomial time complexity via constraints on words
Patrick Baillot
Prepublication LIPN Universite Paris Nord 200302
Abstract:
Light Affine Logic (LAL) is a system due to Girard and Asperti capturing the
complexity class P in a prooftheoretical approach based on linear logic. LAL
provides a typing for lambdacalculus which guarantees that a welltyped
program is executable in polynomialtime on any input.
We prove that the LAL type inference problem for lambdacalculus is decidable
(for propositional LAL). To establish this result we reformulate the type
assignement system into an equivalent one which makes use of subtyping and is
more flexible. We then use a reduction to a satisfiability problem for a system
of inequations on words over a binary alphabet, for which we provide a solving
algorithm.

Message envoye par IMP: http://horde.org/imp/
LIPN  CNRS UMR 7030  http://wwwlipn.univparis13.fr