Vincent Atassi ; Patrick Baillot ; Kazushige Terui - 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 - https://doi.org/10.2168/LMCS-3(4:10)2007
Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine LogicArticle

Authors: Vincent Atassi ; Patrick Baillot ; Kazushige Terui

    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.


    Volume: Volume 3, Issue 4
    Published on: November 15, 2007
    Imported on: January 6, 2007
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.4.1,F.2.2,D.1.1

    12 Documents citing this article

    Consultation statistics

    This page has been seen 1250 times.
    This article's PDF has been downloaded 370 times.