Edit Profile Tatsuta, Makoto Compute Distance To: Compute Author ID: tatsuta.makoto Published as: Tatsuta, Makoto Documents Indexed: 36 Publications since 1991 all top 5 Co-Authors 10 single-authored 8 Berardi, Stefano 4 Nakazawa, Koji 3 Dezani-Ciancaglini, Mariangiola 3 Kimura, Daisuke 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 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 2 The Journal of Symbolic Logic 2 Logical Methods in Computer Science 1 Information and Computation 1 International Journal of Foundations of Computer Science 1 Archive for Mathematical Logic 1 ACM Transactions on Computational Logic Fields 30 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 23 Publications have been cited 47 times in 40 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 6 2008 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 06720997Berardi, Stefano; Tatsuta, Makoto 4 2017 Program synthesis using realizability. Zbl 0745.68030Tatsuta, Makoto 4 1991 Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068Tatsuta, Makoto 3 2007 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, Makoto 3 2007 Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060Nakazawa, Koji; Tatsuta, Makoto 3 2003 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 2 2016 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 A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057Tatsuta, Makoto; Mints, Grigori 2 2005 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 Uniqueness of normal proofs of minimal formulas. Zbl 0791.03004Tatsuta, Makoto 2 1993 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 1 2016 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054Kimura, Daisuke; Tatsuta, Makoto 1 2013 Non-commutative infinitary Peano arithmetic. Zbl 1247.03122Tatsuta, Makoto; Berardi, Stefano 1 2011 On isomorphisms of intersection types. Zbl 1351.03007Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto 1 2010 Non-commutative first-order sequent calculus. Zbl 1257.03049Tatsuta, Makoto 1 2009 Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027Nakazawa, Koji; Tatsuta, Makoto 1 2008 A behavioural model for Klop’s calculus. Zbl 1276.03015Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto 1 2007 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 Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028Tatsuta, Makoto 1 1992 Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 06720997Berardi, Stefano; Tatsuta, Makoto 4 2017 Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan 2 2016 Completeness for recursive procedures in separation logic. Zbl 1339.68044Faisal Al Ameen, Mahmudul; Tatsuta, Makoto 1 2016 Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054Kimura, Daisuke; Tatsuta, Makoto 1 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 6 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 3 2007 Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019Berardi, Stefano; Tatsuta, 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 3 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 59 Authors 10 Tatsuta, Makoto 5 Berardi, Stefano 5 Fujita, Ken-etsu 4 Nakazawa, Koji 3 Schubert, Aleksy 2 Nakano, Hiroshi 2 Takayama, Yukihide 1 Broda, Sabine 1 Brown, Chad Edward 1 Chai, Guorong 1 Chen, Taolue 1 Chin, Wei-Ngan 1 Coppo, Mario 1 Coquand, Thierry 1 Damas, Luís 1 Das, Anupam 1 David, René 1 de’Liguoro, Ugo 1 Devesas Campos, Marco 1 Dezani-Ciancaglini, Mariangiola 1 Eades, Harley III 1 Espírito Santo, José Carlos 1 Faisal Al Ameen, Mahmudul 1 Fiore, Marcelo P. 1 Hasegawa, Ryu 1 Hayashi, Susumu 1 Higuchi, Kenichi 1 Ikeda, Satoshi 1 Kameyama, Yukiyoshi 1 Kihara, Toshiaki 1 Kimura, Daisuke 1 Kobayashi, Satoshi 1 Krishnan, Sanjeevi 1 Le, Quang Loc 1 Lellmann, Björn 1 Li, Qiuli 1 Margaria, Ines 1 Matthes, Ralph 1 Mccleeary, Ryan 1 Nour, Karim 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 Studer, Thomas 1 Stump, Aaron 1 Sun, Jun 1 Tsukada, Yasuyuki 1 Tupailo, Sergei 1 Wen, Yanyan 1 Wood, Carol 1 Wu, Zhilin 1 Yamagata, Yoriyuki 1 Zacchi, Maddalena 1 Zhang, Zhe George all top 5 Cited in 12 Serials 8 Annals of Pure and Applied Logic 7 Theoretical Computer Science 3 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 all top 5 Cited in 7 Fields 33 Mathematical logic and foundations (03-XX) 21 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