| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9655876 | Electronic Notes in Theoretical Computer Science | 2005 | 20 Pages |
Abstract
Light Affine Lambda Calculus is a term calculus for polynomial time computation ([K. Terui. Light affine lambda calculus and polytime strong normalization. In Proceedings of LICS'01, pages 209-220, 2001]). Some of the terms of Light Affine Lambda Calculus must however be regarded as errors. Intuitionistic Light Affine Logic (ILAL) types only terms without errors, but not all of them. We introduce two type assignment systems with intersection types : in the first one, typable pseudo-terms are exactly the terms without errors ; in the second one, they are exactly those that reduce to normal terms without errors.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Daniel de Carvalho,