Computer Science – Logic in Computer Science
Scientific paper
2007-10-05
LMCS 3 (4:10) 2007
Computer Science
Logic in Computer Science
32 pages, 8 figures
Scientific paper
10.2168/LMCS-3(4:10)2007
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.
Atassi Vincent
Baillot Patrick
Terui Kazushige
No associations
LandOfFree
Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-328759