Makoto Tatsuta

67 papers A* 5B 15Misc 2Journal 33Unranked 12

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Core Calculus for Type-safe Product Lines of C Programs. CoRR Ferruccio Damiani, Daisuke Kimura, Luca Paolini, Makoto Tatsuta
2026	J	`jnl`	Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs. CoRR Sohei Ito, Makoto Tatsuta
2025	J	`jnl`	Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic. CoRR Sohei Ito, Makoto Tatsuta
2025	J	`jnl`	The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions. J. Log. Comput. Yukihiro Oda, James Brotherston, Makoto Tatsuta
2024	B	`conf`	Representation of Peano Arithmetic in Separation Logic. FSCD Sohei Ito, Makoto Tatsuta
2021	J	`jnl`	Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions. CoRR Yukihiro Masuoka, Makoto Tatsuta
2021	J	`jnl`	Decidability for Entailments of Symbolic Heaps with Arrays. Log. Methods Comput. Sci. Daisuke Kimura, Makoto Tatsuta
2021	B	`conf`	Function Pointer Eliminator for C Programs. APLAS Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa
2019	J	`jnl`	Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. Stefano Berardi, Makoto Tatsuta
2019	J	`jnl`	Completeness and expressiveness of pointer program verification by separation logic. Inf. Comput. Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
2019	B	`conf`	Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. APLAS Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
2018	J	`jnl`	Completeness of Cyclic Proofs for Symbolic Heaps. CoRR Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
2018	J	`jnl`	Decidability for Entailments of Symbolic Heaps with Arrays. CoRR Daisuke Kimura, Makoto Tatsuta
2018	—	`conf`	Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. CMCS Stefano Berardi, Makoto Tatsuta
2017	—	`conf`	A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. CAV (2) Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin
2017	J	`jnl`	Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). NII Shonan Meet. Rep. Marieke Huisman, Thomas Noll, Makoto Tatsuta
2017	J	`jnl`	Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. CoRR Stefano Berardi, Makoto Tatsuta
2017	B	`conf`	Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS Stefano Berardi, Makoto Tatsuta
2017	B	`conf`	Decision Procedure for Entailment of Symbolic Heaps with Arrays. APLAS Daisuke Kimura, Makoto Tatsuta
2017	J	`jnl`	Decision Procedure for Entailment of Symbolic Heaps with Arrays. CoRR Daisuke Kimura, Makoto Tatsuta
2017	J	`jnl`	Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. CoRR Stefano Berardi, Makoto Tatsuta
2017	A*	`conf`	Equivalence of inductive definitions and cyclic proofs under arithmetic. LICS Stefano Berardi, Makoto Tatsuta
2017	—	`conf`	Micro-clustering by data polishing. IEEE BigData Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, Makoto Tatsuta
2016	J	`jnl`	Completeness for recursive procedures in separation logic. Theor. Comput. Sci. Mahmudul Faisal Al Ameen, Makoto Tatsuta
2016	B	`conf`	Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. APLAS Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin
2015	J	`jnl`	Micro-Clustering: Finding Small Clusters in Large Diversity. CoRR Takeaki Uno, Hiroki Maegawa, Takanobu Nakahara, Yukinobu Hamuro, Ryo Yoshinaka, Makoto Tatsuta
2015	B	`conf`	Separation Logic with Monadic Inductive Definitions and Implicit Existentials. APLAS Makoto Tatsuta, Daisuke Kimura
2014	B	`conf`	Completeness of Separation Logic with Inductive Definitions for Program Verification. SEFM Makoto Tatsuta, Wei-Ngan Chin
2013	J	`jnl`	Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types Log. Methods Comput. Sci. Daisuke Kimura, Makoto Tatsuta
2013	—	`conf`	Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. TLCA Stefano Berardi, Makoto Tatsuta
2012	J	`jnl`	Internal models of system F for decompilation. Theor. Comput. Sci. Stefano Berardi, Makoto Tatsuta
2012	J	`jnl`	Verification of Substitution Theorem Using HOL. Inf. Media Technol. Takayuki Koai, Makoto Tatsuta
2011	B	`conf`	Non-Commutative Infinitary Peano Arithmetic. CSL Makoto Tatsuta, Stefano Berardi
2011	A*	`conf`	Static analysis of multi-staged programs via unstaging translation. POPL Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta
2011	—	`conf`	Type Inference for Bimorphic Recursion GandALF Makoto Tatsuta, Ferruccio Damiani
2011	J	`jnl`	Type checking and typability in domain-free lambda calculi. Theor. Comput. Sci. Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
2010	J	`jnl`	Inhabitation of polymorphic and existential types. Ann. Pure Appl. Log. Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
2010	Misc	`conf`	Internal Normalization, Compilation and Decompilation for System FLOPS Stefano Berardi, Makoto Tatsuta
2010	J	`jnl`	On isomorphisms of intersection types. ACM Trans. Comput. Log. Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
2010	J	`jnl`	Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. Chic. J. Theor. Comput. Sci. Koji Nakazawa, Makoto Tatsuta
2009	B	`conf`	Completeness of Pointer Program Verification by Separation Logic. SEFM Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
2009	—	`conf`	Dual Calculus with Inductive and Coinductive Types. RTA Daisuke Kimura, Makoto Tatsuta
2009	B	`conf`	Non-Commutative First-Order Sequent Calculus. CSL Makoto Tatsuta
2009	—	`conf`	Type Checking and Inference for Polymorphic and Existential Types. CATS Koji Nakazawa, Makoto Tatsuta
2008	B	`conf`	On Isomorphisms of Intersection Types. CSL Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
2008	J	`jnl`	Strong normalization of classical natural deduction with disjunctions. Ann. Pure Appl. Log. Koji Nakazawa, Makoto Tatsuta
2008	Misc	`conf`	Types for Hereditary Head Normalizing Terms. FLOPS Makoto Tatsuta
2008	A*	`conf`	Types for Hereditary Permutators. LICS Makoto Tatsuta
2008	B	`conf`	Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. CSL Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
2007	B	`conf`	Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS Stefano Berardi, Makoto Tatsuta
2007	—	`conf`	Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. TLCA Makoto Tatsuta
2007	—	`conf`	The Maximum Length of Mu-Reduction in Lambda Mu-Calculus. RTA Makoto Tatsuta
2006	—	`conf`	A Behavioural Model for Klop's Calculus. LMCS Mariangiola Dezani-Ciancaglini, Makoto Tatsuta
2006	A*	`conf`	Normalisation is Insensible to lambda-Term Identity or Difference. LICS Makoto Tatsuta, Mariangiola Dezani-Ciancaglini
2005	J	`jnl`	A simple proof of second-order strong normalization with permutative conversions. Ann. Pure Appl. Log. Makoto Tatsuta, Grigori Mints
2003	J	`jnl`	Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". J. Symb. Log. Koji Nakazawa, Makoto Tatsuta
2003	J	`jnl`	Strong normalization proof with CPS-translation for second order classical natural deduction. J. Symb. Log. Koji Nakazawa, Makoto Tatsuta
1998	A*	`conf`	Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. LICS Makoto Tatsuta
1998	B	`conf`	Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. MPC Makoto Tatsuta
1997	J	`jnl`	The function ë Arch. Math. Log. Mitsuru Tada, Makoto Tatsuta
1994	J	`jnl`	Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. Theor. Comput. Sci. Makoto Tatsuta
1994	J	`jnl`	Realizability Interpretation of Generalized Inductive Definitions. Theor. Comput. Sci. Satoshi Kobayashi, Makoto Tatsuta
1994	J	`jnl`	Two Realizability Interpretations of Monotone Inductive Definitions. Int. J. Found. Comput. Sci. Makoto Tatsuta
1993	J	`jnl`	Uniqueness of Normal Proofs of Minimal Formulas. J. Symb. Log. Makoto Tatsuta
1992	—	`conf`	Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. FGCS Makoto Tatsuta
1991	—	`conf`	Monotone Recursive Definition of Predicates and Its Realizability Interpretation. TACS Makoto Tatsuta
1991	J	`jnl`	Program Synthesis Using Realizability. Theor. Comput. Sci. Makoto Tatsuta