Edit Profile (opens in new tab) Tatsuta, Makoto Co-Author Distance Author ID: tatsuta.makoto Published as: Tatsuta, Makoto Documents Indexed: 42 Publications since 1991 Co-Authors: 22 Co-Authors with 31 Joint Publications 448 Co-Co-Authors all top 5 Co-Authors 11 single-authored 9 Berardi, Stefano 5 Kimura, Daisuke 4 Nakazawa, Koji 3 Chin, Wei-Ngan 3 Dezani-Ciancaglini, Mariangiola 3 Nakano, Hiroshi 2 Di Cosmo, Roberto 2 Faisal Al Ameen, Mahmudul 2 Giovannetti, Elio 2 Kameyama, Yukiyoshi 1 Aktemur, Barış 1 Choi, Wontae 1 Damiani, Ferruccio 1 Fujita, Ken-etsu 1 Hasegawa, Ryu 1 Kobayashi, Satoshi 1 Le, Quang Loc 1 Mints, Grigoriĭ Efroimovich 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 38 Mathematical logic and foundations (03-XX) 25 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 33 Publications have been cited 90 times in 71 Documents Cited by ▼ Year ▼ Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 1486.03094Berardi, Stefano; Tatsuta, Makoto 12 2017 Program synthesis using realizability. Zbl 0745.68030Tatsuta, Makoto 6 1991 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068Tatsuta, Makoto 6 2007 Undecidability of type-checking in domain-free typed lambda-calculi with existence. Zbl 1156.03316Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi 5 2008 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129Berardi, Stefano; Tatsuta, Makoto 5 2017 A decidable fragment in separation logic with inductive predicates and arithmetic. Zbl 1497.03048Quang Loc Le; Tatsuta, Makoto; Sun, Jun; Chin, Wei-Ngan 5 2017 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, Makoto 4 2007 Realizability interpretation of generalized inductive definitions. Zbl 0801.03022Kobayashi, Satoshi; Tatsuta, Makoto 4 1994 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060Nakazawa, Koji; Tatsuta, Makoto 4 2003 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 1485.03078Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 3 2016 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 3 2016 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070Tatsuta, Makoto; Kimura, Daisuke 3 2015 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 1509.03158Berardi, Stefano; Tatsuta, Makoto 3 2019 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004Tatsuta, Makoto 2 1993 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054Kimura, Daisuke; Tatsuta, Makoto 2 2013 Inhabitation of polymorphic and existential types. Zbl 1225.03034Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi 2 2010 Dual calculus with inductive and coinductive types. Zbl 1242.03085Kimura, Daisuke; Tatsuta, Makoto 2 2009 Realizability for constructive theory of functions and classes and its application to program synthesis. Zbl 0945.03558Tatsuta, Makoto 2 1998 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057Tatsuta, Makoto; Mints, Grigori 2 2005 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 1520.03008Berardi, Stefano; Tatsuta, Makoto 2 2018 On isomorphisms of intersection types. Zbl 1351.03007Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 A behavioural model for Klop’s calculus. Zbl 1276.03015Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 Types for hereditary head normalizing terms. Zbl 1138.68021Tatsuta, Makoto 1 2008 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027Nakazawa, Koji; Tatsuta, Makoto 1 2008 Non-commutative first-order sequent calculus. Zbl 1257.03049Tatsuta, Makoto 1 2009 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0801.68027Tatsuta, Makoto 1 1994 Two realizability interpretations of monotone inductive definitions. Zbl 0802.03027Tatsuta, Makoto 1 1994 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028Tatsuta, Makoto 1 1992 Decidability for entailments of symbolic heaps with arrays. Zbl 07350781Kimura, Daisuke; Tatsuta, Makoto 1 2021 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122Tatsuta, Makoto; Berardi, Stefano 1 2011 Monotone recursive definition of predicates and its realizability interpretation. Zbl 1493.68124Tatsuta, Makoto 1 1991 Decision procedure for entailment of symbolic heaps with arrays. Zbl 1503.68045Kimura, Daisuke; Tatsuta, Makoto 1 2017 Decidability for entailments of symbolic heaps with arrays. Zbl 07350781Kimura, Daisuke; Tatsuta, Makoto 1 2021 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 1509.03158Berardi, Stefano; Tatsuta, Makoto 3 2019 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 1520.03008Berardi, Stefano; Tatsuta, Makoto 2 2018 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 1486.03094Berardi, Stefano; Tatsuta, Makoto 12 2017 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129Berardi, Stefano; Tatsuta, Makoto 5 2017 A decidable fragment in separation logic with inductive predicates and arithmetic. Zbl 1497.03048Quang Loc Le; Tatsuta, Makoto; Sun, Jun; Chin, Wei-Ngan 5 2017 Decision procedure for entailment of symbolic heaps with arrays. Zbl 1503.68045Kimura, Daisuke; Tatsuta, Makoto 1 2017 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 1485.03078Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 3 2016 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 3 2016 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070Tatsuta, Makoto; Kimura, Daisuke 3 2015 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054Kimura, Daisuke; Tatsuta, Makoto 2 2013 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122Tatsuta, Makoto; Berardi, Stefano 1 2011 Inhabitation of polymorphic and existential types. Zbl 1225.03034Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi 2 2010 On isomorphisms of intersection types. Zbl 1351.03007Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 Dual calculus with inductive and coinductive types. Zbl 1242.03085Kimura, Daisuke; Tatsuta, Makoto 2 2009 Non-commutative first-order sequent calculus. Zbl 1257.03049Tatsuta, Makoto 1 2009 Undecidability of type-checking in domain-free typed lambda-calculi with existence. Zbl 1156.03316Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi 5 2008 Types for hereditary head normalizing terms. Zbl 1138.68021Tatsuta, Makoto 1 2008 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027Nakazawa, Koji; Tatsuta, Makoto 1 2008 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068Tatsuta, Makoto 6 2007 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, Makoto 4 2007 A behavioural model for Klop’s calculus. Zbl 1276.03015Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057Tatsuta, Makoto; Mints, Grigori 2 2005 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060Nakazawa, Koji; Tatsuta, Makoto 4 2003 Realizability for constructive theory of functions and classes and its application to program synthesis. Zbl 0945.03558Tatsuta, Makoto 2 1998 Realizability interpretation of generalized inductive definitions. Zbl 0801.03022Kobayashi, Satoshi; Tatsuta, Makoto 4 1994 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0801.68027Tatsuta, Makoto 1 1994 Two realizability interpretations of monotone inductive definitions. Zbl 0802.03027Tatsuta, Makoto 1 1994 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004Tatsuta, Makoto 2 1993 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028Tatsuta, Makoto 1 1992 Program synthesis using realizability. Zbl 0745.68030Tatsuta, Makoto 6 1991 Monotone recursive definition of predicates and its realizability interpretation. Zbl 1493.68124Tatsuta, Makoto 1 1991 all cited Publications top 5 cited Publications all top 5 Cited by 94 Authors 15 Tatsuta, Makoto 6 Berardi, Stefano 6 Nakazawa, Koji 5 Fujita, Ken-etsu 5 Kimura, Daisuke 3 Das, Anupam 3 Le, Quang Loc 3 Nakano, Hiroshi 3 Schubert, Aleksy 2 Afshari, Bahareh 2 Cao, Yongzhi 2 Cohen, Liron 2 Girlando, Marianna 2 Hasegawa, Ryu 2 Jin, Zhao 2 Kameyama, Yukiyoshi 2 Kobayashi, Satoshi 2 Riba, Colin 2 Stratulat, Sorin 2 Takayama, Yukihide 2 Wang, Hanpin 2 Zhang, Bowen 1 Barthe, Gilles 1 Broda, Sabine 1 Brown, Chad Edward 1 Cao, Tianyue 1 Chai, Guorong 1 Chen, Taolue 1 Chin, Wei-Ngan 1 Coppo, Mario 1 Coquand, Thierry 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 Espírito Santo, José Carlos 1 Faisal Al Ameen, Mahmudul 1 Fiore, Marcelo P. 1 Grégoire, Benjamin 1 Hayashi, Susumu 1 Hetzl, Stefan 1 Ikeda, Satoshi 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 Matthes, Ralph 1 Mccleeary, Ryan 1 Menéndez Turata, Guillermo 1 Mordido, Andreia 1 Nollet, Rémi 1 Nour, Karim 1 Pagel, Jens 1 Pailos, Federico Matias 1 Pfenning, Frank 1 Pham, Long H. 1 Phan, Quoc-Sang 1 Pinto, Luís F. 1 Qin, Shengchao 1 Rizkallah, Christine 1 Rowe, Reuben N. S. 1 Saotome, Kenji 1 Sato, Masahiko 1 Saurin, Alexis 1 Simpson, Alex K. 1 Song, Fu 1 Studer, Thomas 1 Stump, Aaron 1 Sun, Jun 1 Tasson, Christine 1 Tsukada, Yasuyuki 1 Tupailo, Sergei 1 Vial, Pierre 1 Vierling, Jannik 1 Wehr, Dominik 1 Wen, Yanyan 1 Wood, Carol 1 Wu, Zhilin 1 Yamagata, Yoriyuki 1 Zacchi, Maddalena 1 Zhang, Lei 1 Zhang, Zhe George 1 Zuleger, Florian all top 5 Cited in 15 Serials 9 Theoretical Computer Science 9 Annals of Pure and Applied Logic 5 Logical Methods in Computer Science 2 Information and Computation 2 MSCS. Mathematical Structures in Computer Science 1 Information Processing Letters 1 The Journal of Symbolic Logic 1 Journal of Symbolic Computation 1 Journal of Automated Reasoning 1 International Journal of Foundations of Computer Science 1 Applied Categorical Structures 1 The Bulletin of Symbolic Logic 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Combinatorial Optimization 1 Logic and Logical Philosophy all top 5 Cited in 7 Fields 59 Mathematical logic and foundations (03-XX) 40 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