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)

   Volume 11 (2015)

   Volume 12 (2016)

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

Creative Commons