Sciweavers

CORR
2004
Springer

Light types for polynomial time computation in lambda-calculus

13 years 3 months ago
Light types for polynomial time computation in lambda-calculus
We present a polymorphic type system for lambda calculus ensuring that welltyped programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL. Key words: linear logic, light linear logic, lambda calculus, type system, implicit computational complexity, polynomial time complexity.
Patrick Baillot, Kazushige Terui
Added 17 Dec 2010
Updated 17 Dec 2010
Type Journal
Year 2004
Where CORR
Authors Patrick Baillot, Kazushige Terui
Comments (0)