Verification of Ptime reducibility for system F terms via Dual Light Affine Logic
| dc.creator | Atassi, Vincent | |
| dc.creator | Baillot, Patrick | |
| dc.creator | Terui, Kazushige | |
| dc.date | 2006-03-27 | |
| dc.date.accessioned | 2026-07-07T07:05:55Z | |
| dc.date.available | 2026-07-07T07:05:55Z | |
| dc.description | In a previous work we introduced Dual Light Affine Logic (DLAL) ([BaillotTerui04]) 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 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, finds all possible ways to decorate it into a DLAL typed term. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term. | |
| dc.description | 21 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0603104 | |
| dc.identifier | http://arxiv.org/abs/cs/0603104 | |
| dc.identifier | A paraître dans Proceedings Computer Science Logic 2006 (CSL'06), LNCS, Springer. (2006) | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/109840 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Verification of Ptime reducibility for system F terms via Dual Light Affine Logic | |
| dc.type | text |