Atassi, Vincent and Baillot, Patrick and Terui, Kazushige - Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

lmcs:1234 - Logical Methods in Computer Science, November 15, 2007, Volume 3, Issue 4
Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

Authors: Atassi, Vincent and Baillot, Patrick and Terui, Kazushige

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.


Source : oai:arXiv.org:0710.1153
DOI : 10.2168/LMCS-3(4:10)2007
Volume: Volume 3, Issue 4
Published on: November 15, 2007
Submitted on: January 6, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.4.1,F.2.2,D.1.1


Share

Consultation statistics

This page has been seen 157 times.
This article's PDF has been downloaded 42 times.