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

new paper on type inference in light logic


I would like to announce the availability of the following paper at:

     http://www-lipn.univ-paris13.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 2003-02

 Abstract:
  Light Affine Logic (LAL) is a system due to Girard and Asperti capturing the 
complexity class P in a proof-theoretical approach based on linear logic. LAL 
provides a typing for lambda-calculus which guarantees that a well-typed
 program is executable in polynomial-time on any input. 
 We prove that the LAL type inference problem for lambda-calculus 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://www-lipn.univ-paris13.fr