Edit Profile (opens in new tab) Tatsuta, Makoto Compute Distance To: Compute Author ID: tatsuta.makoto Published as: Tatsuta, Makoto Documents Indexed: 39 Publications since 1991 Co-Authors: 20 Co-Authors with 29 Joint Publications 383 Co-Co-Authors all top 5 Co-Authors 10 single-authored 9 Berardi, Stefano 4 Kimura, Daisuke 4 Nakazawa, Koji 3 Dezani-Ciancaglini, Mariangiola 3 Nakano, Hiroshi 2 Chin, Wei-Ngan 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 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 34 Mathematical logic and foundations (03-XX) 23 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 28 Publications have been cited 58 times in 50 Documents Cited by ▼ Year ▼ Undecidability of type-checking in domain-free typed lambda-calculi with existence. Zbl 1156.03316Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi 5 2008 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 06720997Berardi, Stefano; Tatsuta, Makoto 5 2017 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060Nakazawa, Koji; Tatsuta, Makoto 4 2003 Program synthesis using realizability. Zbl 0745.68030Tatsuta, Makoto 4 1991 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, Makoto 4 2007 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068Tatsuta, Makoto 3 2007 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 3 2016 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057Tatsuta, Makoto; Mints, Grigori 2 2005 Realizability interpretation of generalized inductive definitions. Zbl 0801.03022Kobayashi, Satoshi; Tatsuta, Makoto 2 1994 Realizability for constructive theory of functions and classes and its application to program synthesis. Zbl 0945.03558Tatsuta, Makoto 2 1998 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004Tatsuta, Makoto 2 1993 Dual calculus with inductive and coinductive types. Zbl 1242.03085Kimura, Daisuke; Tatsuta, Makoto 2 2009 Inhabitation of polymorphic and existential types. Zbl 1225.03034Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi 2 2010 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 2 2016 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070Tatsuta, Makoto; Kimura, Daisuke 2 2015 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054Kimura, Daisuke; Tatsuta, Makoto 2 2013 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028Tatsuta, Makoto 1 1992 Two realizability interpretations of monotone inductive definitions. Zbl 0802.03027Tatsuta, Makoto 1 1994 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0801.68027Tatsuta, Makoto 1 1994 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129Berardi, Stefano; Tatsuta, Makoto 1 2017 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 06962930Berardi, Stefano; Tatsuta, Makoto 1 2018 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 07089071Berardi, Stefano; Tatsuta, Makoto 1 2019 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 On isomorphisms of intersection types. Zbl 1351.03007Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122Tatsuta, Makoto; Berardi, Stefano 1 2011 A behavioural model for Klop’s calculus. Zbl 1276.03015Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal 1 2019 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 07089071Berardi, Stefano; Tatsuta, Makoto 1 2019 Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 06962930Berardi, Stefano; Tatsuta, Makoto 1 2018 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 06720997Berardi, Stefano; Tatsuta, Makoto 5 2017 Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129Berardi, Stefano; Tatsuta, Makoto 1 2017 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 3 2016 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 2 2016 Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070Tatsuta, Makoto; Kimura, Daisuke 2 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 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027Nakazawa, Koji; Tatsuta, Makoto 1 2008 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, Makoto 4 2007 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068Tatsuta, Makoto 3 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 2 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 0801.68027Tatsuta, 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 4 1991 all cited Publications top 5 cited Publications all top 5 Cited by 70 Authors 11 Tatsuta, Makoto 5 Berardi, Stefano 5 Fujita, Ken-etsu 4 Nakazawa, Koji 3 Kimura, Daisuke 3 Schubert, Aleksy 2 Hasegawa, Ryu 2 Le, Quang Loc 2 Nakano, Hiroshi 2 Takayama, Yukihide 1 Afshari, Bahareh 1 Broda, Sabine 1 Brown, Chad Edward 1 Cao, Yongzhi 1 Chai, Guorong 1 Chen, Taolue 1 Chin, Wei-Ngan 1 Cohen, Liron 1 Coppo, Mario 1 Coquand, Thierry 1 Damas, Luís 1 Das, Anupam 1 David, Rene 1 de’Liguoro, Ugo 1 Devesas Campos, Marco 1 Dezani-Ciancaglini, Mariangiola 1 Eades, Harley III 1 Espírito Santo, José 1 Faisal Al Ameen, Mahmudul 1 Fiore, Marcelo P. 1 Hayashi, Susumu 1 Ikeda, Satoshi 1 Jin, Zhao 1 Kakutani, Yoshihiko 1 Kameyama, Yukiyoshi 1 Kobayashi, Satoshi 1 Krishnan, Sanjeevi 1 Leigh, Graham Emil 1 Lellmann, Björn 1 Li, Qiuli 1 Margaria, Ines 1 Matthes, Ralph 1 Mccleeary, Ryan 1 Menéndez Turata, Guillermo 1 Nour, Karim 1 Pagel, Jens 1 Pailos, Federico Matias 1 Pham, Long H. 1 Phan, Quoc-Sang 1 Pinto, Luís F. 1 Qin, Shengchao 1 Riba, Colin 1 Rizkallah, Christine 1 Simpson, Alex K. 1 Song, Fu 1 Stratulat, Sorin 1 Studer, Thomas 1 Stump, Aaron 1 Sun, Jun 1 Tsukada, Yasuyuki 1 Tupailo, Sergei 1 Wang, Hanpin 1 Wen, Yanyan 1 Wood, Carol 1 Wu, Zhilin 1 Yamagata, Yoriyuki 1 Zacchi, Maddalena 1 Zhang, Bowen 1 Zhang, Zhe George 1 Zuleger, Florian all top 5 Cited in 13 Serials 8 Theoretical Computer Science 8 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 International Journal of Foundations of Computer Science 1 Applied Categorical Structures 1 The Bulletin of Symbolic Logic 1 Journal of Combinatorial Optimization 1 Logic and Logical Philosophy all top 5 Cited in 7 Fields 43 Mathematical logic and foundations (03-XX) 25 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