Monotone Recursive Definition of Predicates and Its Realizability Interpretation. - Makoto Tatsuta (TACS, 1991)

Program Synthesis Using Realizability. - Makoto Tatsuta (Theor. Comput. Sci., 1991)

Uniqueness of Normal Proofs of Minimal Formulas. - Makoto Tatsuta (J. Symb. Log., 1993)

Two Realizability Interpretations of Monotone Inductive Definitions. - Makoto Tatsuta (Int. J. Found. Comput. Sci., 1994)

Realizability Interpretation of Generalized Inductive Definitions. - Satoshi Kobayashi; Makoto Tatsuta (Theor. Comput. Sci., 1994)

Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. - Makoto Tatsuta (Theor. Comput. Sci., 1994)

The function ëa/mû lfloor a/m floor in sharply bounded arithmetic. - Mitsuru Tada; Makoto Tatsuta (Arch. Math. Log., 1997)

Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. - Makoto Tatsuta (LICS, 1998)

Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. - Makoto Tatsuta (MPC, 1998)

Strong normalization proof with CPS-translation for second order classical natural deduction. - Koji Nakazawa; Makoto Tatsuta (J. Symb. Log., 2003)

Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". - Koji Nakazawa; Makoto Tatsuta (J. Symb. Log., 2003)

A simple proof of second-order strong normalization with permutative conversions. - Makoto Tatsuta; Grigori Mints (Ann. Pure Appl. Log., 2005)

Normalisation is Insensible to lambda-Term Identity or Difference. - Makoto Tatsuta; Mariangiola Dezani-Ciancaglini (LICS, 2006)

A Behavioural Model for Klop's Calculus. - Mariangiola Dezani-Ciancaglini; Makoto Tatsuta (LMCS, 2006)

Positive Arithmetic Without Exchange Is a Subclassical Logic. - Stefano Berardi; Makoto Tatsuta (APLAS, 2007)

The Maximum Length of Mu-Reduction in Lambda Mu-Calculus. - Makoto Tatsuta (RTA, 2007)

Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. - Makoto Tatsuta (TLCA, 2007)

Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. - Koji Nakazawa; Makoto Tatsuta; Yukiyoshi Kameyama; Hiroshi Nakano (CSL, 2008)

Types for Hereditary Head Normalizing Terms. - Makoto Tatsuta (FLOPS, 2008)

Types for Hereditary Permutators. - Makoto Tatsuta (LICS, 2008)

Strong normalization of classical natural deduction with disjunctions. - Koji Nakazawa; Makoto Tatsuta (Ann. Pure Appl. Log., 2008)

Type Checking and Inference for Polymorphic and Existential Types. - Koji Nakazawa; Makoto Tatsuta (CATS, 2009)

Non-Commutative First-Order Sequent Calculus. - Makoto Tatsuta (CSL, 2009)

Dual Calculus with Inductive and Coinductive Types. - Daisuke Kimura; Makoto Tatsuta (RTA, 2009)

Completeness of Pointer Program Verification by Separation Logic. - Makoto Tatsuta; Wei-Ngan Chin; Mahmudul Faisal Al Ameen (SEFM, 2009)

Internal Normalization, Compilation and Decompilation for System Fbh. - Stefano Berardi; Makoto Tatsuta (FLOPS, 2010)

Inhabitation of polymorphic and existential types. - Makoto Tatsuta; Ken-etsu Fujita; Ryu Hasegawa; Hiroshi Nakano (Ann. Pure Appl. Log., 2010)

Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. - Koji Nakazawa; Makoto Tatsuta (Chic. J. Theor. Comput. Sci., 2010)

On isomorphisms of intersection types. - Mariangiola Dezani-Ciancaglini; Roberto Di Cosmo; Elio Giovannetti; Makoto Tatsuta (ACM Trans. Comput. Log., 2010)

Non-Commutative Infinitary Peano Arithmetic. - Makoto Tatsuta; Stefano Berardi (CSL, 2011)

Static analysis of multi-staged programs via unstaging translation. - Wontae Choi; Baris Aktemur; Kwangkeun Yi; Makoto Tatsuta (POPL, 2011)

Type Inference for Bimorphic Recursion - Makoto Tatsuta; Ferruccio Damiani (GandALF, 2011)

Type checking and typability in domain-free lambda calculi. - Koji Nakazawa; Makoto Tatsuta; Yukiyoshi Kameyama; Hiroshi Nakano (Theor. Comput. Sci., 2011)

Verification of Substitution Theorem Using HOL. - Takayuki Koai; Makoto Tatsuta (Inf. Media Technol., 2012)

Internal models of system F for decompilation. - Stefano Berardi; Makoto Tatsuta (Theor. Comput. Sci., 2012)

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. - Stefano Berardi; Makoto Tatsuta (TLCA, 2013)

Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types - Daisuke Kimura; Makoto Tatsuta (Log. Methods Comput. Sci., 2013)

Completeness of Separation Logic with Inductive Definitions for Program Verification. - Makoto Tatsuta; Wei-Ngan Chin (SEFM, 2014)

Separation Logic with Monadic Inductive Definitions and Implicit Existentials. - Makoto Tatsuta; Daisuke Kimura (APLAS, 2015)

Micro-Clustering: Finding Small Clusters in Large Diversity. - Takeaki Uno; Hiroki Maegawa; Takanobu Nakahara; Yukinobu Hamuro; Ryo Yoshinaka; Makoto Tatsuta (CoRR, 2015)

Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. - Makoto Tatsuta; Quang Loc Le; Wei-Ngan Chin (APLAS, 2016)

Completeness for recursive procedures in separation logic. - Mahmudul Faisal Al Ameen; Makoto Tatsuta (Theor. Comput. Sci., 2016)

Decision Procedure for Entailment of Symbolic Heaps with Arrays. - Daisuke Kimura; Makoto Tatsuta (APLAS, 2017)

Micro-clustering by data polishing. - Takeaki Uno; Hiroki Maegawa; Takanobu Nakahara; Yukinobu Hamuro; Ryo Yoshinaka; Makoto Tatsuta (IEEE BigData, 2017)

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. - Quang Loc Le; Makoto Tatsuta; Jun Sun 001; Wei-Ngan Chin (CAV (2), 2017)

Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. - Stefano Berardi; Makoto Tatsuta (FoSSaCS, 2017)

Equivalence of inductive definitions and cyclic proofs under arithmetic. - Stefano Berardi; Makoto Tatsuta (LICS, 2017)

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. - Stefano Berardi; Makoto Tatsuta (CoRR, 2017)

Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). - Marieke Huisman; Thomas Noll 001; Makoto Tatsuta (NII Shonan Meet. Rep., 2017)

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. - Stefano Berardi; Makoto Tatsuta (CMCS, 2018)

Completeness of Cyclic Proofs for Symbolic Heaps. - Makoto Tatsuta; Koji Nakazawa; Daisuke Kimura (CoRR, 2018)

Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. - Makoto Tatsuta; Koji Nakazawa; Daisuke Kimura (APLAS, 2019)

Completeness and expressiveness of pointer program verification by separation logic. - Makoto Tatsuta; Wei-Ngan Chin; Mahmudul Faisal Al Ameen (Inf. Comput., 2019)

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. - Stefano Berardi; Makoto Tatsuta (Log. Methods Comput. Sci., 2019)

Function Pointer Eliminator for C Programs. - Daisuke Kimura; Mahmudul Faisal Al Ameen; Makoto Tatsuta; Koji Nakazawa (APLAS, 2021)

Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions. - Yukihiro Masuoka; Makoto Tatsuta (CoRR, 2021)

Decidability for Entailments of Symbolic Heaps with Arrays. - Daisuke Kimura; Makoto Tatsuta (Log. Methods Comput. Sci., 2021)

Representation of Peano Arithmetic in Separation Logic. - Sohei Ito; Makoto Tatsuta (FSCD, 2024)

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions. - Yukihiro Oda; James Brotherston; Makoto Tatsuta (J. Log. Comput., 2025)

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic. - Sohei Ito; Makoto Tatsuta (CoRR, 2025)