3 papers
cs.LO2018
MacNeille completion and Buchholz' Omega rule for parameter-free second order logics
Kazushige Terui
Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it fr…
cs.LO2006
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…
cs.LO2004
A feasible algorithm for typing in Elementary Affine Logic
Patrick Baillot, Kazushige Terui
We give a new type inference algorithm for typing lambda-terms in Elementary Affine Logic (EAL), which is motivated by applications to complexity and optimal reduction. Following p…