Makoto Tatsuta

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 22

Top Topics

Deductive Reasoning

Fixed Point Semantics

Top Venues

Log. Methods Comput. Sci.

Publications

Sohei Ito, Makoto Tatsuta
Representation of Peano Arithmetic in Separation Logic. FSCD (2024)
Hiromasa Hori, Koji Nakazawa, Makoto Tatsuta
Cut elimination for propositional cyclic proof systems with fixed-point operators. CoRR (2023)
Yukihiro Masuoka, Makoto Tatsuta
Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions. CoRR (2021)
Daisuke Kimura, Makoto Tatsuta
Decidability for Entailments of Symbolic Heaps with Arrays. Log. Methods Comput. Sci. 17 (2) (2021)
Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa
Function Pointer Eliminator for C Programs. APLAS (2021)
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. APLAS (2019)
Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
Completeness and expressiveness of pointer program verification by separation logic. Inf. Comput. 267 (2019)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. 15 (3) (2019)
Daisuke Kimura, Makoto Tatsuta
Decidability for Entailments of Symbolic Heaps with Arrays. CoRR (2018)
Stefano Berardi, Makoto Tatsuta
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. CMCS (2018)
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Completeness of Cyclic Proofs for Symbolic Heaps. CoRR (2018)
Stefano Berardi, Makoto Tatsuta
Equivalence of inductive definitions and cyclic proofs under arithmetic. LICS (2017)
Marieke Huisman, Thomas Noll, Makoto Tatsuta
Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). NII Shonan Meet. Rep. 2017 (2017)
Stefano Berardi, Makoto Tatsuta
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. CoRR (2017)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. CoRR (2017)
Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. CAV (2) (2017)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS (2017)
Daisuke Kimura, Makoto Tatsuta
Decision Procedure for Entailment of Symbolic Heaps with Arrays. APLAS (2017)
Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, Makoto Tatsuta
Micro-clustering by data polishing. IEEE BigData (2017)
Daisuke Kimura, Makoto Tatsuta
Decision Procedure for Entailment of Symbolic Heaps with Arrays. CoRR (2017)
Mahmudul Faisal Al Ameen, Makoto Tatsuta
Completeness for recursive procedures in separation logic. Theor. Comput. Sci. 631 (2016)
Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin
Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. APLAS (2016)
Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, Makoto Tatsuta
Micro-Clustering: Finding Small Clusters in Large Diversity. CoRR (2015)
Makoto Tatsuta, Daisuke Kimura
Separation Logic with Monadic Inductive Definitions and Implicit Existentials. APLAS (2015)
Makoto Tatsuta, Wei-Ngan Chin
Completeness of Separation Logic with Inductive Definitions for Program Verification. SEFM (2014)
Stefano Berardi, Makoto Tatsuta
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. TLCA (2013)
Daisuke Kimura, Makoto Tatsuta
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types Log. Methods Comput. Sci. 9 (1) (2013)
Stefano Berardi, Makoto Tatsuta
Internal models of system F for decompilation. Theor. Comput. Sci. 435 (2012)
Takayuki Koai, Makoto Tatsuta
Verification of Substitution Theorem Using HOL. Inf. Media Technol. 7 (2) (2012)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
Type checking and typability in domain-free lambda calculi. Theor. Comput. Sci. 412 (44) (2011)
Makoto Tatsuta, Stefano Berardi
Non-Commutative Infinitary Peano Arithmetic. CSL (2011)
Makoto Tatsuta, Ferruccio Damiani
Type Inference for Bimorphic Recursion GandALF (2011)
Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta
Static analysis of multi-staged programs via unstaging translation. POPL (2011)
Koji Nakazawa, Makoto Tatsuta
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. Chic. J. Theor. Comput. Sci. 2010 (2010)
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
On isomorphisms of intersection types. ACM Trans. Comput. Log. 11 (4) (2010)
Stefano Berardi, Makoto Tatsuta
. FLOPS (2010)
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
Inhabitation of polymorphic and existential types. Ann. Pure Appl. Log. 161 (11) (2010)
Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
Completeness of Pointer Program Verification by Separation Logic. SEFM (2009)
Daisuke Kimura, Makoto Tatsuta
Dual Calculus with Inductive and Coinductive Types. RTA (2009)
Koji Nakazawa, Makoto Tatsuta
Type Checking and Inference for Polymorphic and Existential Types. CATS (2009)
Makoto Tatsuta
Non-Commutative First-Order Sequent Calculus. CSL (2009)
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
On Isomorphisms of Intersection Types. CSL (2008)
Makoto Tatsuta
Types for Hereditary Head Normalizing Terms. FLOPS (2008)
Makoto Tatsuta
Types for Hereditary Permutators. LICS (2008)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. CSL (2008)
Koji Nakazawa, Makoto Tatsuta
Strong normalization of classical natural deduction with disjunctions. Ann. Pure Appl. Log. 153 (1-3) (2008)
Makoto Tatsuta
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. TLCA (2007)
Mariangiola Dezani-Ciancaglini, Makoto Tatsuta
A Behavioural Model for Klop's Calculus. Electron. Notes Theor. Comput. Sci. 169 (2007)
Stefano Berardi, Makoto Tatsuta
Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS (2007)
Makoto Tatsuta
The Maximum Length of Mu-Reduction in Lambda Mu-Calculus. RTA (2007)
Makoto Tatsuta, Mariangiola Dezani-Ciancaglini
Normalisation is Insensible to lambda-Term Identity or Difference. LICS (2006)
Makoto Tatsuta, Grigori Mints
A simple proof of second-order strong normalization with permutative conversions. Ann. Pure Appl. Log. 136 (1-2) (2005)
Koji Nakazawa, Makoto Tatsuta
Strong normalization proof with CPS-translation for second order classical natural deduction. J. Symb. Log. 68 (3) (2003)
Koji Nakazawa, Makoto Tatsuta
Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". J. Symb. Log. 68 (4) (2003)
Makoto Tatsuta
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. MPC (1998)
Makoto Tatsuta
Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. LICS (1998)
Mitsuru Tada, Makoto Tatsuta
û\lfloor a/m\rfloor in sharply bounded arithmetic. Arch. Math. Log. 37 (1) (1997)
Satoshi Kobayashi, Makoto Tatsuta
Realizability Interpretation of Generalized Inductive Definitions. Theor. Comput. Sci. 131 (1) (1994)
Makoto Tatsuta
Two Realizability Interpretations of Monotone Inductive Definitions. Int. J. Found. Comput. Sci. 5 (1) (1994)
Makoto Tatsuta
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. Theor. Comput. Sci. 122 (1&2) (1994)
Makoto Tatsuta
Uniqueness of Normal Proofs of Minimal Formulas. J. Symb. Log. 58 (3) (1993)
Makoto Tatsuta
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. FGCS (1992)
Makoto Tatsuta
Monotone Recursive Definition of Predicates and Its Realizability Interpretation. TACS (1991)
Makoto Tatsuta
Program Synthesis Using Realizability. Theor. Comput. Sci. 90 (2) (1991)