Makoto Tatsuta

J-GLOBAL         Last updated: Mar 5, 2019 at 19:00
 
Avatar
Name
Makoto Tatsuta

Research Areas

 
 

Awards & Honors

 
Apr 2017
EATCS Award for ETAPS best paper, European Association for Theoretical Computer Science (EATCS)
Winner: Stefano Berardi and Makoto Tatsuta
 

Published Papers

 
Completeness and Expressiveness of Pointer Program Verification by Separation Logic
Makoto Tatsuta, Wei-Ngan Chin, and Mahmudul Faisal Al Ameen
Information and Computation   to appear    2019   [Refereed]
Spatial Factorization in Cyclic-Proof System for Separation Logic
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura
Proceedings of the 21st JSSST Workshop on Programming and Programming Languages (PPL2019)   1-28   Mar 2019   [Refereed]
Cyclic Theorem Prover for Separation Logic by Magic Wand
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura,
Proceedings of 1st Workshop on Automated Deduction for Separation Logics (ADSL 2018)   19 pages   Jul 2018   [Refereed]
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence between Inductive Definitions and Cyclic Proofs
Stefano Berardi and Makoto Tatsuta
Lecture Notes in Computer Science   11202 13-33   Apr 2018   [Refereed]
Decidability of Entailments in Separation Logic with Arrays and Lists
Daisuke Kimura, Makoto Tatsuta
Proceedings of the 20th JSSST Workshop on Programming and Programming Languages (PPL2018)   1-16   Mar 2018   [Refereed]
Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, and Makoto Tatsuta
Proceedings of 2017 IEEE International Conference on Big Data (Big Data 2017)   1-7   Dec 2017   [Refereed]
Decision Procedure for Entailment of Symbolic Heaps with Arrays
Makoto Tatsuta
Lecture Notes in Computer Science   10695 169-189   Dec 2017   [Refereed]
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin
Proceedings of 29th International Conference on Computer-Aided Verification (CAV2017)      Jul 2017   [Refereed]
Stefano Berardi and Makoto Tatsuta
Proceedings of Thirty-Second Annual IEEE Symposium on Logic in Computer Science (LICS2017)   1-12   Jun 2017   [Refereed]
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System
Stefano Berardi and Makoto Tatsuta
Lecture Notes in Computer Science      Apr 2017   [Refereed]
Decision Procedure for Symbolic Heaps with Arrays
Daisuke Kimura, Makoto Tatsuta
Proceedings of the 19th JSSST Workshop on Programming and Programming Languages (PPL2017)      Mar 2017   [Refereed]
Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin
Lecture Notes in Computer Science   10017 1-21   Nov 2016   [Refereed]
Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic
Makoto Tatsuta and Daisuke Kimura
Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2016)   1-15   Mar 2016   [Refereed]
Mahmudul Faisal Al Ameen and Makoto Tatsuta
Theoretical Computer Science      2016   [Refereed]
Makoto Tatsuta and Daisuke Kimura
Lecture Notes in Computer Science   9458 69-89   Nov 2015   [Refereed]
Makoto Tatsuta and Wei-Ngan Chin
Lecture Notes in Computer Science   8702 20-34   Sep 2014   [Refereed]
Stefano Berardi and Makoto Tatsuta
Lecture Notes in Computer Science   7941 61-76   Jun 2013   [Refereed]
Daisuke Kimura and Makoto Tatsuta
Logical Methods in Computer Science   9(1) Article 14   Jan 2013   [Refereed]
Daisuke Kimura and Makoto Tatsuta
9(1) Article 14   Jan 2013   [Refereed]
Stefano Berardi and Makoto Tatsuta
Theoretical Computer Science   435 3-20   Jun 2012   [Refereed]
Takayuki Koai and Makoto Tatsuta
Information Processing Society of Japan Transactions on Programming   5(2) 88-96   Mar 2012   [Refereed]
Makoto Tatsuta and Stefano Berardi
Leibniz International Proceedings in Informatics   12 538-552   Sep 2011   [Refereed]
Type Inference for Bimorphic Recursion
Makoto Tatsuta and Ferruccio Damiani
Electronic Proceedings in Theoretical Computer Science   102-115   Jun 2011   [Refereed]
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
Theoretical Computer Science   412(44) 6193-6207   Mar 2011   [Refereed]
Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta
Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages   46(1) 81-92   Jan 2011   [Refereed]
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti and Makoto Tatsuta
ACM Transactions on Computational Logic   11(4) Article 25   Jul 2010   [Refereed]
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano
Annals of Pure and Applied Logic   161(11) 1390-1399   Jun 2010   [Refereed]
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems
Koji Nakazawa and Makoto Tatsuta
Chicago Journal of Theoretical Computer Science   Article 7   Apr 2010   [Refereed]
Stefano Berardi and Makoto Tatsuta
Lecture Notes in Computer Science   6009 207-223   Apr 2010   [Refereed]
M. Tatsuta, W.N. Chin, and M.F. Al Ameen
Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009)   179-188   Nov 2009   [Refereed]
Makoto Tatsuta
Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009), Lecture Notes in Computer Science   5771 470-484   Sep 2009   [Refereed]
Daisuke Kimura and Makoto Tatsuta
Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA 09), Lecture Notes in Computer Science   5595 224-238   Jun 2009   [Refereed]
Type Checking and Inference for Polymorphic and Existential Types (共著)
Koji Nakazawa and Makoto Tatsuta
Proceedings of The 15th Computing: The Australasian Theory Symposium (CATS2009), Conferences in Research and Practice in Information Technology   94 61-69   Jan 2009   [Refereed]
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science   5213 461-477   Sep 2008   [Refereed]
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science   5213 478-492   Sep 2008   [Refereed]
Second-Order Logic without Implication nor Disjunction
Makoto Tatsuta
Proceedings of 10th Asian Logic Conference (ALC 10), Bulletin of Symbolic Logic      Sep 2008   [Refereed]
Inhabitance of Existential Types is Decidable in Negation-Product Fragment (共著)
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano
Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC2008)      Jul 2008   [Refereed]
Makoto Tatsuta
Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS2008)   83-92   Jun 2008   [Refereed]
Some Non-Recursively-Enumerable Sets and Their Types
Makoto Tatsuta
Proceedings of Workshop on Constructivism: Logic and Mathematics      May 2008   [Invited]
Makoto Tatsuta
Proceedings of Ninth International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science   4989 195-209   Apr 2008   [Refereed]
Koji Nakazawa, Makoto Tatsuta
Annals of Pure and Applied Logic      Apr 2008   [Refereed]
Types for Hereditary Permutators
Makoto Tatsuta
NII Technical Report      Nov 2007
Positive Arithmetic without Exchange is a Subclassical Logic
Stefano Berardi, Makoto Tatsuta
Lecture Notes in Computer Science   4807 271-285   Nov 2007   [Refereed]
The maximum length of mu-reduction in lambda mu-calculus (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science   4533 359-373   Jun 2007   [Refereed]
Simple saturated sets for disjunction and second-order existential quantification (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science   4583 366-380   Jun 2007   [Refereed]
Uniqueness of D-normal Proofs
Makoto Tatsuta
NII Technical Report   (NII-20)    Dec 2006
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science   327-336   Aug 2006   [Refereed]
Normalisation is Insensible to lambda-term Identity or Difference
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
NII Technical Report   (NII-20)    Mar 2006
Mariangiola Dezani-Ciancaglini and Makoto Tatsuta
Proceedings of Logic, Model and Computer Science 2006, Electronic Notes in Theoretical Computer Science 169   19-32   Mar 2006   [Refereed]
M. Tatsuta
Progress in Informatics   (2) 41-56   Dec 2005   [Refereed]
M. Tatsuta and G. Mints
Annals of Pure and Applied Logic   136(39449) 134-155   Dec 2004   [Refereed]
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction
K. Nakazawa and M. Tatsuta
Journal Symbolic of Logic   68(3) 851-859   Sep 2003   [Refereed]
Long D-normal form yields uniqueness of proofs
S. Hirokawa and M. Tatsuta
Proceedings of 2000 European Congress of Association for Symbolic Logic      Aug 2000   [Refereed]
Uniqueness of D-normal Proofs
M. Tatsuta
Proceedings of 7th Asian Logic Conference   41-42   Jun 1999   [Refereed]
Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science   358-367   Jun 1998   [Refereed]
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422   338-364   Jun 1998   [Refereed]
Uniform Continuity of Graph Model and Partial Function Model
M. Tatsuta
Proceedings of 1997-98 Annual Meeting of Association for Symbolic Logic   20-21   May 1998   [Refereed]
The Function [a/m] in Sharply Bounded Arithmetic
M. Tada and M. Tatsuta
Archive for Mathematical Logic   37 51-57   Jul 1997   [Refereed]
S. Kobayashi and M. Tatsuta
Theoretical Computer Science   131(1) 121-138   Aug 1994   [Refereed]
M. Tatsuta
International Journal of Foundations of Computer Science   5(1) 1-21   Jun 1994   [Refereed]
M. Tatsuta
Theoretical Computer Science   122(1/2) 119-136   Jan 1994   [Refereed]
Uniqueness of Normal Proofs of Minimal Formulas
M. Tatsuta
Journal of Symbolic Logic   58(3) 789-799   Sep 1993   [Refereed]
Realizability of Inductive Definitions for Constructive Programming (Doctoral Dissertation)
Makoto Tatsuta
博士論文      Mar 1993   [Refereed]
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams
M. Tatsuta
Proceedings of International Conference on Fifth Generation Computer Systems   666-673   Jun 1992   [Refereed]
M. Tatsuta
Theoretical Computer Science   90(2) 309-353   Dec 1991   [Refereed]
Monotone Recursive Definition of Predicates and Its Realizability Interpretation
M. Tatsuta
Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526   526 38-52   Sep 1991   [Refereed]

Conference Activities & Talks

 
Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs [Invited]
Makoto Tatsuta
Invited Lecture, School of Informatics, Aristotle University of Thessaloniki   23 Apr 2018   
Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
Makoto Tatsuta
Second Workshop on Mathematical Logic and its Applications (MLA 2018)   5 Mar 2018   
Program Analysis and Verification by Separation Logic
Makoto Tatsuta
NII Shonan Meeting on Analysis and Verification of Pointer Programs   2 Oct 2017   
Decidability in Symbolic-Heap System with Arithmetic and Arrays
Makoto Tatsuta
Continuity, Computability, Constructivity: From Logic to Algorithms (CCC 2017)   26 Jun 2017   
Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
Makoto Tatsuta
19 Apr 2017   
Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
Makoto Tatsuta
PPLV Seminar   28 Mar 2017   
Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions
Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa
2nd Workshop on New and Emerging Results in Programming Languages and Systems   24 Nov 2016   
Decidable subsystem of Presburger Arithmetic with Inductive Definitions and Application to Symbolic Heaps
Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin
International Workshop on Mathematics for Computation (M4C)   8 May 2016   
Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions
Makoto Tatsuta and Daisuke Kimura
Proceedings of Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)   16 Sep 2015   
Realizability of inductive and coinductive definitions [Invited]
Makoto Tatsuta
JAIST Logic Workshop Series 2015: Constructivism and Computability   3 Mar 2015   
New complete system of Hoare's logic with recursive procedures
M.F. Al Ameen and M. Tatsuta
JAIST Logic Workshop Series 2015: Constructivism and Computability   3 Mar 2015   
Infinite reductions are insensible to lambda-term identity or difference
Mariangiola Dezani and Makoto Tatsuta
Infinity Symposium, March 21--22, 2006, Vrije Universiteit Amsterdam   21 Mar 2006   
Different Substitution Theorem
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Workshop on Linear Logic, Proof Theory and Computer Science, March 16--17, 2006, Keio University   16 Mar 2006   
Martin-Lof's type theory with permutative reductions
M. Tatsuta
Stanford Logic Seminar   18 May 2004   
A simple proof of strong normalization with permutative conversions
M. Tatsuta and G. Mints
Stanford Logic Seminar   3 Feb 2004   

Committee Memberships

 
Mar 2016
 - 
Dec 2017
Fourteenth International Symposium on Functional and Logic Programming (FLOPS 2018)  General chair
 
Sep 2014
 - 
Sep 2015
EACSL Annual Conference on Computer Science Logic (CSL2015)  program committee