Vincent Atassi ; Patrick Baillot ; Kazushige Terui
-
Verification of Ptime Reducibility for system F Terms: Type Inference
in<br> Dual Light Affine Logic
Verification of Ptime Reducibility for system F Terms: Type Inference
in<br> Dual Light Affine LogicArticle
Authors: Vincent Atassi ; Patrick Baillot ; Kazushige Terui
NULL##NULL##NULL
Vincent Atassi;Patrick Baillot;Kazushige Terui
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.
Loris D'Antoni;Marco Gaboardi;Emilio Jesús Gallego Arias;Andreas Haeberlen;et al., Sensitivity analysis using type-based constraints, pp. 43-50, 2013, Boston Massachusetts USA, 10.1145/2505351.2505353.
Emanuele Cesena;Marco Pedicini;Luca Roversi, arXiv (Cornell University), Typing a Core Binary-Field Arithmetic in a Light Logic, pp. 19-35, 2012, 10.1007/978-3-642-32495-6_2.
Olha Shkaravska;Marko van Eekelen;Alejandro Tamalet, Data Archiving and Networked Services (DANS), Collected Size Semantics for Functional Programs over Lists, pp. 118-137, 2011, 10.1007/978-3-642-24452-0_7, http://hdl.handle.net/2066/72040.