The Community for Technology Leaders
RSS Icon
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
13 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool