July 17, 2004 to July 17, 2004
Patrick Baillot , Universit? Paris-Nord, France
Kazushige Terui , National Institute of Informatics, Tokyo, Japan
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.
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