| Autor: |
Vincent Atassi, Patrick Baillot, Kazushige Terui |
| Jazyk: |
angličtina |
| Rok vydání: |
2007 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Vol Volume 3, Issue 4 (2007) |
| Druh dokumentu: |
article |
| ISSN: |
1860-5974 |
| DOI: |
10.2168/LMCS-3(4:10)2007 |
| Popis: |
In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, determines whether it is typable in DLAL and outputs a concrete typing if there exists any. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
