Verification of Ptime reducibility for system F terms via Dual Light Affine Logic

Vincent Atassi, Patrick Baillot, Kazushige Terui

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-calc…