some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

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: 8488

Creative Commons