Subscribe

Turku, Finland

July 17, 2004 to July 17, 2004

ISBN: 0-7695-2192-4

pp: 266-275

Patrick Baillot , Universit? Paris-Nord, France

Kazushige Terui , National Institute of Informatics, Tokyo, Japan

ABSTRACT

We propose a new type system for lambda-calculus ensuring that well-typed 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: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DLAL allows to represent all polytime functions.

INDEX TERMS

null

CITATION

Patrick Baillot,
Kazushige Terui,
"Light Types for Polynomial Time Computation in Lambda-Calculus",

*LICS*, 2004, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science 2004, pp. 266-275, doi:10.1109/LICS.2004.1319621