Edit Profile (opens in new tab) Tatsuta, Makoto Co-Author Distance Author ID: tatsuta.makoto Published as: Tatsuta, Makoto Documents Indexed: 46 Publications since 1991, including 3 Additional arXiv Preprints Co-Authors: 24 Co-Authors with 35 Joint Publications 454 Co-Co-Authors all top 5 Co-Authors 11 single-authored 10 Berardi, Stefano 6 Kimura, Daisuke 6 Nakazawa, Koji 3 Chin, Wei-Ngan 3 Dezani-Ciancaglini, Mariangiola 3 Nakano, Hiroshi 2 Al Ameen, Mahmudul Faisal 2 Di Cosmo, Roberto 2 Giovannetti, Elio 2 Kameyama, Yukiyoshi 1 Aktemur, Barış 1 Choi, Wontae 1 Damiani, Ferruccio 1 Fujita, Ken-etsu 1 Hasegawa, Ryu 1 Hori, Hiromasa 1 Kobayashi, Satoshi 1 Le, Quang Loc 1 Mints, Grigoriĭ Efroimovich 1 Oda, Yukihiro 1 Quang Loc Le 1 Sun, Jun 1 Tada, Mitsuru 1 Yi, Kwangkeun all top 5 Serials 6 Theoretical Computer Science 3 Annals of Pure and Applied Logic 3 Logical Methods in Computer Science 2 The Journal of Symbolic Logic 1 Information and Computation 1 International Journal of Foundations of Computer Science 1 Archive for Mathematical Logic 1 ACM Transactions on Computational Logic Fields 40 Mathematical logic and foundations (03-XX) 26 Computer science (68-XX) 1 Order, lattices, ordered algebraic structures (06-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 35 Publications have been cited 114 times in 85 Documents Cited by ▼ Year ▼ Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 1486.03094 Berardi, Stefano; Tatsuta, Makoto 13 2017 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129 Berardi, Stefano; Tatsuta, Makoto 10 2017 A decidable fragment in separation logic with inductive predicates and arithmetic. Zbl 1497.03048 Quang Loc Le; Tatsuta, Makoto; Sun, Jun; Chin, Wei-Ngan 8 2017 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068 Tatsuta, Makoto 7 2007 Program synthesis using realizability. Zbl 0745.68030 Tatsuta, Makoto 6 1991 Undecidability of type-checking in domain-free typed lambda-calculi with existence. Zbl 1156.03316 Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi 5 2008 Completeness of cyclic proofs for symbolic heaps with inductive definitions. Zbl 1542.68038 Tatsuta, Makoto; Nakazawa, Koji; Kimura, Daisuke 5 2019 Realizability interpretation of generalized inductive definitions. Zbl 0801.03022 Kobayashi, Satoshi; Tatsuta, Makoto 4 1994 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060 Nakazawa, Koji; Tatsuta, Makoto 4 2003 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019 Berardi, Stefano; Tatsuta, Makoto 4 2007 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070 Tatsuta, Makoto; Kimura, Daisuke 4 2015 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 1485.03078 Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 4 2016 Inhabitation of polymorphic and existential types. Zbl 1225.03034 Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi 3 2010 Dual calculus with inductive and coinductive types. Zbl 1242.03085 Kimura, Daisuke; Tatsuta, Makoto 3 2009 Completeness for recursive procedures in separation logic. Zbl 1339.68044 Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 3 2016 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057 Tatsuta, Makoto; Mints, Grigori 3 2005 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 1509.03158 Berardi, Stefano; Tatsuta, Makoto 3 2019 Realizability for constructive theory of functions and classes and its application to program synthesis. Zbl 0945.03558 Tatsuta, Makoto 2 1998 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004 Tatsuta, Makoto 2 1993 Types for hereditary head normalizing terms. Zbl 1138.68021 Tatsuta, Makoto 2 2008 Decision procedure for entailment of symbolic heaps with arrays. Zbl 1503.68045 Kimura, Daisuke; Tatsuta, Makoto 2 2017 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 1520.03008 Berardi, Stefano; Tatsuta, Makoto 2 2018 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054 Kimura, Daisuke; Tatsuta, Makoto 2 2013 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028 Tatsuta, Makoto 2 1992 Non-commutative first-order sequent calculus. Zbl 1257.03049 Tatsuta, Makoto 1 2009 Two realizability interpretations of monotone inductive definitions. Zbl 0802.03027 Tatsuta, Makoto 1 1994 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0801.68027 Tatsuta, Makoto 1 1994 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027 Nakazawa, Koji; Tatsuta, Makoto 1 2008 Monotone recursive definition of predicates and its realizability interpretation. Zbl 1493.68124 Tatsuta, Makoto 1 1991 On isomorphisms of intersection types. Zbl 1351.03007 Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038 Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 A behavioural model for Klop’s calculus. Zbl 1276.03015 Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122 Tatsuta, Makoto; Berardi, Stefano 1 2011 Decidability for entailments of symbolic heaps with arrays. Zbl 1535.03180 Kimura, Daisuke; Tatsuta, Makoto 1 2021 Static analysis of multi-staged programs via unstaging translation. Zbl 1284.68170 Choi, Wontae; Aktemur, Baris; Yi, Kwangkeun; Tatsuta, Makoto 1 2011 Decidability for entailments of symbolic heaps with arrays. Zbl 1535.03180 Kimura, Daisuke; Tatsuta, Makoto 1 2021 Completeness of cyclic proofs for symbolic heaps with inductive definitions. Zbl 1542.68038 Tatsuta, Makoto; Nakazawa, Koji; Kimura, Daisuke 5 2019 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 1509.03158 Berardi, Stefano; Tatsuta, Makoto 3 2019 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038 Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 1520.03008 Berardi, Stefano; Tatsuta, Makoto 2 2018 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 1486.03094 Berardi, Stefano; Tatsuta, Makoto 13 2017 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129 Berardi, Stefano; Tatsuta, Makoto 10 2017 A decidable fragment in separation logic with inductive predicates and arithmetic. Zbl 1497.03048 Quang Loc Le; Tatsuta, Makoto; Sun, Jun; Chin, Wei-Ngan 8 2017 Decision procedure for entailment of symbolic heaps with arrays. Zbl 1503.68045 Kimura, Daisuke; Tatsuta, Makoto 2 2017 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 1485.03078 Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 4 2016 Completeness for recursive procedures in separation logic. Zbl 1339.68044 Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 3 2016 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070 Tatsuta, Makoto; Kimura, Daisuke 4 2015 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054 Kimura, Daisuke; Tatsuta, Makoto 2 2013 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122 Tatsuta, Makoto; Berardi, Stefano 1 2011 Static analysis of multi-staged programs via unstaging translation. Zbl 1284.68170 Choi, Wontae; Aktemur, Baris; Yi, Kwangkeun; Tatsuta, Makoto 1 2011 Inhabitation of polymorphic and existential types. Zbl 1225.03034 Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi 3 2010 On isomorphisms of intersection types. Zbl 1351.03007 Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 Dual calculus with inductive and coinductive types. Zbl 1242.03085 Kimura, Daisuke; Tatsuta, Makoto 3 2009 Non-commutative first-order sequent calculus. Zbl 1257.03049 Tatsuta, Makoto 1 2009 Undecidability of type-checking in domain-free typed lambda-calculi with existence. Zbl 1156.03316 Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi 5 2008 Types for hereditary head normalizing terms. Zbl 1138.68021 Tatsuta, Makoto 2 2008 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027 Nakazawa, Koji; Tatsuta, Makoto 1 2008 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068 Tatsuta, Makoto 7 2007 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019 Berardi, Stefano; Tatsuta, Makoto 4 2007 A behavioural model for Klop’s calculus. Zbl 1276.03015 Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057 Tatsuta, Makoto; Mints, Grigori 3 2005 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060 Nakazawa, Koji; Tatsuta, Makoto 4 2003 Realizability for constructive theory of functions and classes and its application to program synthesis. Zbl 0945.03558 Tatsuta, Makoto 2 1998 Realizability interpretation of generalized inductive definitions. Zbl 0801.03022 Kobayashi, Satoshi; Tatsuta, Makoto 4 1994 Two realizability interpretations of monotone inductive definitions. Zbl 0802.03027 Tatsuta, Makoto 1 1994 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0801.68027 Tatsuta, Makoto 1 1994 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004 Tatsuta, Makoto 2 1993 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028 Tatsuta, Makoto 2 1992 Program synthesis using realizability. Zbl 0745.68030 Tatsuta, Makoto 6 1991 Monotone recursive definition of predicates and its realizability interpretation. Zbl 1493.68124 Tatsuta, Makoto 1 1991 all cited Publications top 5 cited Publications all top 5 Cited by 113 Authors 16 Tatsuta, Makoto 8 Nakazawa, Koji 7 Kimura, Daisuke 6 Berardi, Stefano 6 Fujita, Ken-etsu 4 Das, Anupam 4 Le, Quang Loc 4 Schubert, Aleksy 3 Afshari, Bahareh 3 Nakano, Hiroshi 2 Cao, Yongzhi 2 Chen, Taolue 2 Cohen, Liron 2 Coquand, Thierry 2 Girlando, Marianna 2 Hasegawa, Ryu 2 Jin, Zhao 2 Kameyama, Yukiyoshi 2 Kobayashi, Satoshi 2 Pagel, Jens 2 Peltier, Nicolas 2 Pham, Long H. 2 Phan, Quoc-Sang 2 Riba, Colin 2 Saotome, Kenji 2 Stratulat, Sorin 2 Sun, Jun 2 Takayama, Yukihide 2 Wang, Hanpin 2 Wehr, Dominik 2 Wu, Zhilin 2 Zhang, Bowen 2 Zuleger, Florian 1 Abel, Andreas M. 1 Al Ameen, Mahmudul Faisal 1 Barthe, Gilles 1 Boy de la Tour, Thierry 1 Broda, Sabine 1 Brown, Chad Edward 1 Caferra, Ricardo 1 Cao, Tianyue 1 Cerda, Rémy 1 Chai, Guorong 1 Chin, Wei-Ngan 1 Coppo, Mario 1 Curzi, Gianluca 1 Czajka, Łukasz 1 Damas, Luís 1 Das, Ankush 1 David, Rene 1 de’Liguoro, Ugo 1 Devesas Campos, Marco 1 DeYoung, Henry 1 Dezani-Ciancaglini, Mariangiola 1 Eades, Harley III 1 Echenim, Mnacho 1 Espírito Santo, José Carlos 1 Fiore, Marcelo P. 1 Gao, Chong 1 Grégoire, Benjamin 1 Hayashi, Susumu 1 Hetzl, Stefan 1 Ikeda, Satoshi 1 Inoue, Jun-Ichiro 1 Kakutani, Yoshihiko 1 Kop, Cynthia 1 Krishnan, Sanjeevi 1 Lakhani, Zeeshan 1 Le, Xuan-Bach D. 1 Leigh, Graham Emil 1 Lellmann, Björn 1 Li, Qiuli 1 Mansutti, Alessio 1 Margaria, Ines 1 Matheja, Christoph 1 Matthes, Ralph 1 Mccleeary, Ryan 1 Menéndez Turata, Guillermo 1 Mordido, Andreia 1 Nollet, Rémi 1 Nour, Karim 1 Olivetti, Nicola 1 Pailos, Federico Matias 1 Pfenning, Frank 1 Pientka, Brigitte 1 Pinto, Luís F. 1 Qin, Shengchao 1 Rizkallah, Christine 1 Rowe, Reuben N. S. 1 Sato, Masahiko 1 Saurin, Alexis 1 Schwind, Camilla B. 1 Setzer, Anton 1 Simpson, Alex K. 1 Song, Fu 1 Studer, Thomas 1 Stump, Aaron 1 Taha, Walid 1 Tasson, Christine 1 Thibodeau, David ...and 13 more Authors all top 5 Cited in 18 Serials 10 Theoretical Computer Science 9 Annals of Pure and Applied Logic 6 Logical Methods in Computer Science 3 Mathematical Structures in Computer Science 2 Information and Computation 2 Journal of Automated Reasoning 1 Information Processing Letters 1 The Journal of Symbolic Logic 1 Journal of Symbolic Computation 1 International Journal of Foundations of Computer Science 1 Applied Categorical Structures 1 Journal of Applied Non-Classical Logics 1 Journal of Functional Programming 1 The Bulletin of Symbolic Logic 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Combinatorial Optimization 1 Logic and Logical Philosophy 1 ACM Transactions on Computational Logic all top 5 Cited in 7 Fields 71 Mathematical logic and foundations (03-XX) 50 Computer science (68-XX) 1 History and biography (01-XX) 1 Category theory; homological algebra (18-XX) 1 General topology (54-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year