
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
Light Types for Polynomial Time Computation in LambdaCalculus
Turku, Finland
July 13July 17
ISBN: 0769521924
ASCII Text  x  
Patrick Baillot, Kazushige Terui, "Light Types for Polynomial Time Computation in LambdaCalculus," Logic in Computer Science, Symposium on, pp. 266275, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004.  
BibTex  x  
@article{ 10.1109/LICS.2004.1319621, author = {Patrick Baillot and Kazushige Terui}, title = {Light Types for Polynomial Time Computation in LambdaCalculus}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2004}, issn = {10436871}, pages = {266275}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2004.1319621}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  CONF JO  Logic in Computer Science, Symposium on TI  Light Types for Polynomial Time Computation in LambdaCalculus SN  10436871 SP266 EP275 A1  Patrick Baillot, A1  Kazushige Terui, PY  2004 KW  null VL  0 JA  Logic in Computer Science, Symposium on ER   
We propose a new type system for lambdacalculus 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 lambdaterms: subject reduction is satisfied and a welltyped term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DLAL allows to represent all polytime functions.
Citation:
Patrick Baillot, Kazushige Terui, "Light Types for Polynomial Time Computation in LambdaCalculus," lics, pp.266275, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.