Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

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…