| |
VOLUME 3, ISSUE 4, PAPER 10
|
Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
|
©Vincent Atassi, University Paris 13 / CNRS
©Patrick Baillot, University Paris 13 / CNRS
©Kazushige Terui, National Institute of Informatics, Tokyo
|
Abstract
In a previous work Baillot and Terui introduced Dual light affine logic (DLAL)
as a variant of Light linear logic suitable for guaranteeing
complexity properties on lambda calculus terms: all typable terms can be
evaluated in polynomial time by beta reduction and all Ptime functions can be
represented. In the present work we address the problem of typing lambda-terms
in second-order DLAL. For that we give a procedure which, starting with a term
typed in system F, determines whether it is typable in DLAL and outputs a
concrete typing if there exists any. We show that our procedure can be run in
time polynomial in the size of the original Church typed system F term.
|
Publication date: November 15, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(4:10)2007
Hit Counts: 4464 |
 Creative Commons | |
