×
Compute Distance To:
Author ID: tatsuta.makoto Recent zbMATH articles by "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

Publications by Year

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.03316
Nakazawa, 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 06720997
Berardi, Stefano; Tatsuta, Makoto
5
2017
Strong normalization proof with CPS-translation for second order classical natural deduction. Zbl 1058.03060
Nakazawa, Koji; Tatsuta, Makoto
4
2003
Program synthesis using realizability. Zbl 0745.68030
Tatsuta, Makoto
4
1991
Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019
Berardi, Stefano; Tatsuta, Makoto
4
2007
Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068
Tatsuta, Makoto
3
2007
Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504
Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan
3
2016
A simple proof of second-order strong normalization with permutative conversions. Zbl 1095.03057
Tatsuta, Makoto; Mints, Grigori
2
2005
Realizability interpretation of generalized inductive definitions. Zbl 0801.03022
Kobayashi, Satoshi; Tatsuta, Makoto
2
1994
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
Dual calculus with inductive and coinductive types. Zbl 1242.03085
Kimura, Daisuke; Tatsuta, Makoto
2
2009
Inhabitation of polymorphic and existential types. Zbl 1225.03034
Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi
2
2010
Completeness for recursive procedures in separation logic. Zbl 1339.68044
Faisal Al Ameen, Mahmudul; Tatsuta, Makoto
2
2016
Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070
Tatsuta, Makoto; Kimura, Daisuke
2
2015
Call-by-value and call-by-name dual calculi with inductive and coinductive types. Zbl 1280.03054
Kimura, Daisuke; Tatsuta, Makoto
2
2013
Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038
Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal
1
2019
Realizability interpretation of coinductive definitions and program synthesis with streams. Zbl 0860.03028
Tatsuta, Makoto
1
1992
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
Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129
Berardi, Stefano; Tatsuta, Makoto
1
2017
Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 06962930
Berardi, Stefano; Tatsuta, Makoto
1
2018
Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Zbl 07089071
Berardi, Stefano; Tatsuta, Makoto
1
2019
Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027
Nakazawa, Koji; Tatsuta, Makoto
1
2008
Non-commutative first-order sequent calculus. Zbl 1257.03049
Tatsuta, Makoto
1
2009
On isomorphisms of intersection types. Zbl 1351.03007
Dezani-Ciancaglini, Mariangiola; Di Cosmo, Roberto; Giovannetti, Elio; Tatsuta, Makoto
1
2010
Non-commutative infinitary Peano arithmetic. Zbl 1247.03122
Tatsuta, Makoto; Berardi, Stefano
1
2011
A behavioural model for Klop’s calculus. Zbl 1276.03015
Dezani-Ciancaglini, Mariangiola; Tatsuta, Makoto
1
2007
Completeness and expressiveness of pointer program verification by separation logic. Zbl 1422.68038
Tatsuta, 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 07089071
Berardi, Stefano; Tatsuta, Makoto
1
2019
Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. Zbl 06962930
Berardi, Stefano; Tatsuta, Makoto
1
2018
Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. Zbl 06720997
Berardi, Stefano; Tatsuta, Makoto
5
2017
Equivalence of inductive definitions and cyclic proofs under arithmetic. Zbl 1452.03129
Berardi, Stefano; Tatsuta, Makoto
1
2017
Decision procedure for separation logic with inductive definitions and Presburger arithmetic. Zbl 06667504
Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan
3
2016
Completeness for recursive procedures in separation logic. Zbl 1339.68044
Faisal Al Ameen, Mahmudul; Tatsuta, Makoto
2
2016
Separation logic with monadic inductive definitions and implicit existentials. Zbl 1329.03070
Tatsuta, Makoto; Kimura, Daisuke
2
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
Inhabitation of polymorphic and existential types. Zbl 1225.03034
Tatsuta, Makoto; Fujita, Ken-Etsu; Hasegawa, Ryu; Nakano, Hiroshi
2
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
2
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
Strong normalization of classical natural deduction with disjunctions. Zbl 1141.03027
Nakazawa, Koji; Tatsuta, Makoto
1
2008
Positive arithmetic without exchange is a subclassical logic. Zbl 1138.03019
Berardi, Stefano; Tatsuta, Makoto
4
2007
Simple saturated sets for disjunction and second-order existential quantification. Zbl 1215.03068
Tatsuta, Makoto
3
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
2
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
2
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
1
1992
Program synthesis using realizability. Zbl 0745.68030
Tatsuta, Makoto
4
1991

Citations by Year