47 citations · 88 across the 7 of their papers we have counts for
8 papers
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…
On the meaning of logical completeness
Michele Basaldella, Kazushige Terui
Goedel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. O…
Semantics of Typed Lambda-Calculus with Constructors
Barbara Petit
We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-ca…
Church => Scott = Ptime: an application of resource sensitive realizability
Aloïs Brunel, Kazushige Terui
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed b…
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…
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…