Completeness of Pointer Program Verification by Separation Logic
M. Tatsuta, W.N. Chin, and M.F. Al Ameen
Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009) 179-188 Nov 2009 [Refereed]
Non-Commutative First-Order Sequent Calculus
Makoto Tatsuta
Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009), Lecture Notes in Computer Science 5771 470-484 Sep 2009 [Refereed]
Dual Calculus with Inductive and Coinductive Types (共著)
Daisuke Kimura and Makoto Tatsuta
Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA 09), Lecture Notes in Computer Science 5595 224-238 Jun 2009 [Refereed]
Type Checking and Inference for Polymorphic and Existential Types (共著)
Koji Nakazawa and Makoto Tatsuta
Proceedings of The 15th Computing: The Australasian Theory Symposium (CATS2009), Conferences in Research and Practice in Information Technology 94 61-69 Jan 2009 [Refereed]
On Isomorphisms of Intersection Types (共著)
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 461-477 Sep 2008 [Refereed]
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence (共著)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 478-492 Sep 2008 [Refereed]
Second-Order Logic without Implication nor Disjunction
Makoto Tatsuta
Proceedings of 10th Asian Logic Conference (ALC 10), Bulletin of Symbolic Logic Sep 2008 [Refereed]
Inhabitance of Existential Types is Decidable in Negation-Product Fragment (共著)
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano
Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC2008) Jul 2008 [Refereed]
Types for Hereditary Permutators
Makoto Tatsuta
Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS2008) 83-92 Jun 2008 [Refereed]
Some Non-Recursively-Enumerable Sets and Their Types
Makoto Tatsuta
Proceedings of Workshop on Constructivism: Logic and Mathematics May 2008 [Invited]
Types for Hereditary Head Normalizing Terms
Makoto Tatsuta
Proceedings of Ninth International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science 4989 195-209 Apr 2008 [Refereed]
Strong normalization of classical natural deduction with disjunctions
Koji Nakazawa, Makoto Tatsuta
Annals of Pure and Applied Logic Apr 2008 [Refereed]
Types for Hereditary Permutators
Makoto Tatsuta
NII Technical Report Nov 2007
Positive Arithmetic without Exchange is a Subclassical Logic
Stefano Berardi, Makoto Tatsuta
Lecture Notes in Computer Science 4807 271-285 Nov 2007 [Refereed]
The maximum length of mu-reduction in lambda mu-calculus (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science 4533 359-373 Jun 2007 [Refereed]
Simple saturated sets for disjunction and second-order existential quantification (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science 4583 366-380 Jun 2007 [Refereed]
Uniqueness of D-normal Proofs
Makoto Tatsuta
NII Technical Report (NII-20) Dec 2006
Normalisation is Insensible to lambda-term Identity or Difference, lambda-term Identity or Difference
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science 327-336 Aug 2006 [Refereed]
Normalisation is Insensible to lambda-term Identity or Difference
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
NII Technical Report (NII-20) Mar 2006
A Behavioural Model for Klop's Calculus
Mariangiola Dezani-Ciancaglini and Makoto Tatsuta
Proceedings of Logic, Model and Computer Science 2006, Electronic Notes in Theoretical Computer Science 169 19-32 Mar 2006 [Refereed]
Second order permutative conversions with Prawitz's strong validity
M. Tatsuta
Progress in Informatics 2 41-56 Dec 2005 [Refereed]
A Simple Proof of Second Order Strong Normalization with Permutative Conversions
M. Tatsuta and G. Mints
Annals of Pure and Applied Logic 136(39449) 134-155 Dec 2004 [Refereed]
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction
K. Nakazawa and M. Tatsuta
Journal Symbolic of Logic 68(3) 851-859 Sep 2003 [Refereed]
Long D-normal form yields uniqueness of proofs
S. Hirokawa and M. Tatsuta
Proceedings of 2000 European Congress of Association for Symbolic Logic Aug 2000 [Refereed]
Uniqueness of D-normal Proofs
M. Tatsuta
Proceedings of 7th Asian Logic Conference 41-42 Jun 1999 [Refereed]
Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science 358-367 Jun 1998 [Refereed]
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422 338-364 Jun 1998 [Refereed]
Uniform Continuity of Graph Model and Partial Function Model
M. Tatsuta
Proceedings of 1997-98 Annual Meeting of Association for Symbolic Logic 20-21 May 1998 [Refereed]
The Function [a/m] in Sharply Bounded Arithmetic
M. Tada and M. Tatsuta
Archive for Mathematical Logic 37 51-57 Jul 1997 [Refereed]
Realizability interpretation of generalized inductive definitions
S. Kobayashi and M. Tatsuta
Theoretical Computer Science 131(1) 121-138 Aug 1994 [Refereed]
Two realizability interpretations of monotone inductive definitions
M. Tatsuta
International Journal of Foundations of Computer Science 5(1) 1-21 Jun 1994 [Refereed]
Realizability interpretation of coinductive definitions and program synthesis with streams
M. Tatsuta
Theoretical Computer Science 122 119-136 Jan 1994 [Refereed]
Uniqueness of Normal Proofs of Minimal Formulas
M. Tatsuta
Journal of Symbolic Logic 58(3) 789-799 Sep 1993 [Refereed]
Realizability of Inductive Definitions for Constructive Programming (Doctoral Dissertation)
Makoto Tatsuta
博士論文 Mar 1993 [Refereed]
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams
M. Tatsuta
Proceedings of International Conference on Fifth Generation Computer Systems 666-673 Jun 1992 [Refereed]
Program synthesis using realizability
M. Tatsuta
Theoretical Computer Science 90 309-353 Dec 1991 [Refereed]
Monotone Recursive Definition of Predicates and Its Realizability Interpretation
M. Tatsuta
Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526 526 38-52 Sep 1991 [Refereed]
