The Finite Model Property for Various Fragments of Intuitionistic Linear Logic. - Mitsuhiro Okada; Kazushige Terui (J. Symb. Log., 1999)

Light Affine Calculus and Polytime Strong Normalization. - Kazushige Terui (LICS, 2001)

On the Computational Complexity of Cut-Elimination in Linear Logic. - Harry G. Mairson; Kazushige Terui (ICTCS, 2003)

Proof Nets and Boolean Circuits. - Kazushige Terui (LICS, 2004)

Light Affine Set Theory: A Naive Set Theory of Polynomial Time. - Kazushige Terui (Stud Logica, 2004)

A Feasible Algorithm for Typing in Elementary Affine Logic. - Patrick Baillot; Kazushige Terui (TLCA, 2005)

Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic. - Vincent Atassi; Patrick Baillot; Kazushige Terui (CSL, 2006)

Modular Cut-Elimination: Finding Proofs or Counterexamples. - Agata Ciabattoni; Kazushige Terui (LPAR, 2006)

Intuitionistic phase semantics is almost classical. - Max I. Kanovich; Mitsuhiro Okada; Kazushige Terui (Math. Struct. Comput. Sci., 2006)

Towards a Semantic Characterization of Cut-Elimination. - Agata Ciabattoni; Kazushige Terui (Stud Logica, 2006)

Light affine lambda calculus and polynomial time strong normalization. - Kazushige Terui (Arch. Math. Log., 2007)

Which structural rules admit cut elimination? An algebraic criterion. - Kazushige Terui (J. Symb. Log., 2007)

Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic. - Vincent Atassi; Patrick Baillot; Kazushige Terui (Log. Methods Comput. Sci., 2007)

From Axioms to Analytic Rules in Nonclassical Logics. - Agata Ciabattoni; Nikolaos Galatos; Kazushige Terui (LICS, 2008)

Expanding the Realm of Systematic Proof Theory. - Agata Ciabattoni; Lutz Straßburger; Kazushige Terui (CSL, 2009)

Light types for polynomial time computation in lambda calculus. - Patrick Baillot; Kazushige Terui (Inf. Comput., 2009)

Infinitary Completeness in Ludics. - Michele Basaldella; Kazushige Terui (LICS, 2010)

Church => Scott = Ptime: an application of resource sensitive realizability - Aloïs Brunel; Kazushige Terui (DICE, 2010)

On the meaning of logical completeness - Michele Basaldella; Kazushige Terui (Log. Methods Comput. Sci., 2010)

From Focalization of Logic to the Logic of Focalization. - Michele Basaldella; Alexis Saurin; Kazushige Terui (MFPS, 2010)

Proof Theory and Algebra in Substructural Logics. - Kazushige Terui (TABLEAUX, 2011)

Disjunction property and complexity of substructural logics. - Rostislav Horcík; Kazushige Terui (Theor. Comput. Sci., 2011)

Computational ludics. - Kazushige Terui (Theor. Comput. Sci., 2011)

On the Meaning of Focalization. - Michele Basaldella; Alexis Saurin; Kazushige Terui (PRELUDE Project, 2011)

Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. - Kazushige Terui (RTA, 2012)

Algebraic proof theory for substructural logics: Cut-elimination and completions. - Agata Ciabattoni; Nikolaos Galatos; Kazushige Terui (Ann. Pure Appl. Log., 2012)

Intersection Types for Normalization and Verification (Invited Talk). - Kazushige Terui (FSTTCS, 2013)

Parsimonious Types and Non-uniform Computation. - Damiano Mazza; Kazushige Terui (ICALP (2), 2015)

Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. - Ryota Akiyoshi; Kazushige Terui (FSCD, 2016)

Algebraic proof theory: Hypersequents and hypercompletions. - Agata Ciabattoni; Nikolaos Galatos; Kazushige Terui (Ann. Pure Appl. Log., 2017)

MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics. - Kazushige Terui (CSL, 2018)