default search action
Makoto Tatsuta
Person information
- affiliation: National Institute of Informatics, NII, Japan
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c34]Sohei Ito, Makoto Tatsuta:
Representation of Peano Arithmetic in Separation Logic. FSCD 2024: 18:1-18:17 - 2021
- [j21]Daisuke Kimura, Makoto Tatsuta:
Decidability for Entailments of Symbolic Heaps with Arrays. Log. Methods Comput. Sci. 17(2) (2021) - [c33]Daisuke Kimura, Mahmudul Faisal Al Ameen
, Makoto Tatsuta, Koji Nakazawa:
Function Pointer Eliminator for C Programs. APLAS 2021: 23-37 - [i8]Yukihiro Masuoka, Makoto Tatsuta:
Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions. CoRR abs/2106.11798 (2021)
2010 – 2019
- 2019
- [j20]Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
Completeness and expressiveness of pointer program verification by separation logic. Inf. Comput. 267: 1-27 (2019) - [j19]Stefano Berardi, Makoto Tatsuta:
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. 15(3) (2019) - [c32]Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura:
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. APLAS 2019: 367-387 - 2018
- [c31]Stefano Berardi, Makoto Tatsuta:
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. CMCS 2018: 13-33 - [i7]Daisuke Kimura, Makoto Tatsuta:
Decidability for Entailments of Symbolic Heaps with Arrays. CoRR abs/1802.05935 (2018) - [i6]Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura:
Completeness of Cyclic Proofs for Symbolic Heaps. CoRR abs/1804.03938 (2018) - 2017
- [c30]Daisuke Kimura, Makoto Tatsuta:
Decision Procedure for Entailment of Symbolic Heaps with Arrays. APLAS 2017: 169-189 - [c29]Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka
Micro-clustering by data polishing. IEEE BigData 2017: 1012-1018 - [c28]Quang Loc Le, Makoto Tatsuta, Jun Sun
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. CAV (2) 2017: 495-517 - [c27]Stefano Berardi, Makoto Tatsuta:
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS 2017: 301-317 - [c26]Stefano Berardi, Makoto Tatsuta:
Equivalence of inductive definitions and cyclic proofs under arithmetic. LICS 2017: 1-12 - [i5]Daisuke Kimura, Makoto Tatsuta:
Decision Procedure for Entailment of Symbolic Heaps with Arrays. CoRR abs/1708.06696 (2017) - [i4]Stefano Berardi, Makoto Tatsuta:
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. CoRR abs/1712.03502 (2017) - [i3]Stefano Berardi, Makoto Tatsuta:
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. CoRR abs/1712.09603 (2017) - [i2]Marieke Huisman, Thomas Noll, Makoto Tatsuta:
Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). NII Shonan Meet. Rep. 2017 (2017) - 2016
- [j18]Mahmudul Faisal Al Ameen
Completeness for recursive procedures in separation logic. Theor. Comput. Sci. 631: 73-96 (2016) - [c25]Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin:
Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. APLAS 2016: 423-443 - 2015
- [c24]Makoto Tatsuta, Daisuke Kimura:
Separation Logic with Monadic Inductive Definitions and Implicit Existentials. APLAS 2015: 69-89 - [i1]Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, Makoto Tatsuta:
Micro-Clustering: Finding Small Clusters in Large Diversity. CoRR abs/1507.03067 (2015) - 2014
- [c23]Makoto Tatsuta, Wei-Ngan Chin:
Completeness of Separation Logic with Inductive Definitions for Program Verification. SEFM 2014: 20-34 - 2013
- [j17]Daisuke Kimura, Makoto Tatsuta:
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types. Log. Methods Comput. Sci. 9(1) (2013) - [c22]Stefano Berardi, Makoto Tatsuta:
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. TLCA 2013: 61-76 - 2012
- [j16]Takayuki Koai, Makoto Tatsuta:
Verification of Substitution Theorem Using HOL. Inf. Media Technol. 7(2): 685-693 (2012) - [j15]Stefano Berardi, Makoto Tatsuta:
Internal models of system F for decompilation. Theor. Comput. Sci. 435: 3-20 (2012) - 2011
- [j14]Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano:
Type checking and typability in domain-free lambda calculi. Theor. Comput. Sci. 412(44): 6193-6207 (2011) - [c21]Makoto Tatsuta, Stefano Berardi:
Non-Commutative Infinitary Peano Arithmetic. CSL 2011: 538-552 - [c20]Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta:
Static analysis of multi-staged programs via unstaging translation. POPL 2011: 81-92 - [c19]Makoto Tatsuta, Ferruccio Damiani
Type Inference for Bimorphic Recursion. GandALF 2011: 102-115 - 2010
- [j13]Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano:
Inhabitation of polymorphic and existential types. Ann. Pure Appl. Log. 161(11): 1390-1399 (2010) - [j12]Koji Nakazawa, Makoto Tatsuta:
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. Chic. J. Theor. Comput. Sci. 2010 (2010) - [j11]Mariangiola Dezani-Ciancaglini
On isomorphisms of intersection types. ACM Trans. Comput. Log. 11(4): 25:1-25:24 (2010) - [c18]Stefano Berardi, Makoto Tatsuta:
Internal Normalization, Compilation and Decompilation for System Fbh. FLOPS 2010: 207-223
2000 – 2009
- 2009
- [c17]Koji Nakazawa, Makoto Tatsuta:
Type Checking and Inference for Polymorphic and Existential Types. CATS 2009: 61-69 - [c16]Makoto Tatsuta:
Non-Commutative First-Order Sequent Calculus. CSL 2009: 470-484 - [c15]Daisuke Kimura, Makoto Tatsuta:
Dual Calculus with Inductive and Coinductive Types. RTA 2009: 224-238 - [c14]Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
Completeness of Pointer Program Verification by Separation Logic. SEFM 2009: 179-188 - 2008
- [j10]Koji Nakazawa, Makoto Tatsuta:
Strong normalization of classical natural deduction with disjunctions. Ann. Pure Appl. Log. 153(1-3): 21-37 (2008) - [c13]Mariangiola Dezani-Ciancaglini
On Isomorphisms of Intersection Types. CSL 2008: 461-477 - [c12]Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano:
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. CSL 2008: 478-492 - [c11]Makoto Tatsuta:
Types for Hereditary Head Normalizing Terms. FLOPS 2008: 195-209 - [c10]Makoto Tatsuta:
Types for Hereditary Permutators. LICS 2008: 83-92 - 2007
- [c9]Stefano Berardi, Makoto Tatsuta:
Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS 2007: 271-285 - [c8]Makoto Tatsuta:
The Maximum Length of Mu-Reduction in Lambda Mu-Calculus. RTA 2007: 359-373 - [c7]Makoto Tatsuta:
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. TLCA 2007: 366-380 - 2006
- [c6]Makoto Tatsuta, Mariangiola Dezani-Ciancaglini
Normalisation is Insensible to lambda-Term Identity or Difference. LICS 2006: 327-338 - [c5]Mariangiola Dezani-Ciancaglini
A Behavioural Model for Klop's Calculus. LMCS 2006: 19-32 - 2005
- [j9]Makoto Tatsuta, Grigori Mints:
A simple proof of second-order strong normalization with permutative conversions. Ann. Pure Appl. Log. 136(1-2): 134-155 (2005) - 2003
- [j8]Koji Nakazawa, Makoto Tatsuta:
Strong normalization proof with CPS-translation for second order classical natural deduction. J. Symb. Log. 68(3): 851-859 (2003) - [j7]Koji Nakazawa, Makoto Tatsuta:
Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". J. Symb. Log. 68(4): 1415-1416 (2003)
1990 – 1999
- 1998
- [c4]Makoto Tatsuta:
Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. LICS 1998: 358-367 - [c3]Makoto Tatsuta:
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. MPC 1998: 338-364 - 1997
- [j6]Mitsuru Tada, Makoto Tatsuta:
The function ëa/mû\lfloor a/m\rfloor in sharply bounded arithmetic. Arch. Math. Log. 37(1): 51-57 (1997) - 1994
- [j5]Makoto Tatsuta:
Two Realizability Interpretations of Monotone Inductive Definitions. Int. J. Found. Comput. Sci. 5(1): 1-21 (1994) - [j4]Makoto Tatsuta:
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. Theor. Comput. Sci. 122(1&2): 119-136 (1994) - [j3]Satoshi Kobayashi, Makoto Tatsuta:
Realizability Interpretation of Generalized Inductive Definitions. Theor. Comput. Sci. 131(1): 121-138 (1994) - 1993
- [j2]Makoto Tatsuta:
Uniqueness of Normal Proofs of Minimal Formulas. J. Symb. Log. 58(3): 789-799 (1993) - 1992
- [c2]Makoto Tatsuta:
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. FGCS 1992: 666-673 - 1991
- [j1]Makoto Tatsuta:
Program Synthesis Using Realizability. Theor. Comput. Sci. 90(2): 309-353 (1991) - [c1]Makoto Tatsuta:
Monotone Recursive Definition of Predicates and Its Realizability Interpretation. TACS 1991: 38-52
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-05 20:56 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: