Makoto Tatsuta

Available identifiers

zbMath Open tatsuta.makotoMaRDI QIDQ278746

List of research outcomes

Publication	Date of Publication	Type
Cut elimination for propositional cyclic proof systems with fixed-point operators	2023-12-20	Paper
Decision Procedure for Entailment of Symbolic Heaps with Arrays	2022-12-09	Paper
Monotone recursive definition of predicates and its realizability interpretation	2022-08-16	Paper
A decidable fragment in separation logic with inductive predicates and arithmetic	2022-08-12	Paper
https://portal.mardi4nfdi.de/entity/Q4989410	2021-05-25	Paper
https://portal.mardi4nfdi.de/entity/Q4964722	2021-03-03	Paper
https://portal.mardi4nfdi.de/entity/Q5144661	2021-01-19	Paper
https://portal.mardi4nfdi.de/entity/Q5227521	2019-08-06	Paper
Completeness and expressiveness of pointer program verification by separation logic	2019-05-29	Paper
Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs	2018-10-23	Paper
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic	2017-12-10	Paper
Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System	2017-05-19	Paper
Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic	2016-12-21	Paper
Completeness for recursive procedures in separation logic	2016-05-02	Paper
Separation Logic with Monadic Inductive Definitions and Implicit Existentials	2016-01-08	Paper
On isomorphisms of intersection types	2015-09-17	Paper
Static analysis of multi-staged programs via unstaging translation	2014-04-10	Paper
https://portal.mardi4nfdi.de/entity/Q2863905	2013-12-04	Paper
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics	2013-06-28	Paper
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types	2013-04-09	Paper
https://portal.mardi4nfdi.de/entity/Q2915710	2012-09-18	Paper
Internal models of system F for decompilation	2012-06-25	Paper
Type checking and typability in domain-free lambda calculi	2012-01-04	Paper
Inhabitation of polymorphic and existential types	2011-08-26	Paper
Internal Normalization, Compilation and Decompilation for System ${\mathcal F}_{\beta\eta}$	2010-05-04	Paper
Non-Commutative First-Order Sequent Calculus	2009-11-12	Paper
Dual Calculus with Inductive and Coinductive Types	2009-06-30	Paper
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification	2009-03-10	Paper
On Isomorphisms of Intersection Types	2008-11-20	Paper
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence	2008-11-20	Paper
Positive Arithmetic Without Exchange Is a Subclassical Logic	2008-05-15	Paper
Strong normalization of classical natural deduction with disjunctions	2008-04-24	Paper
Types for Hereditary Head Normalizing Terms	2008-04-11	Paper
The Maximum Length of Mu-Reduction in Lambda Mu-Calculus	2008-01-02	Paper
A simple proof of second-order strong normalization with permutative conversions	2005-09-22	Paper
Strong normalization proof with CPS-translation for second order classical natural deduction	2005-02-09	Paper
https://portal.mardi4nfdi.de/entity/Q4936128	2000-01-24	Paper
The function \(\lfloor a/m\rfloor\) in sharply bounded arithmetic	1998-05-26	Paper
https://portal.mardi4nfdi.de/entity/Q5688910	1997-04-21	Paper
TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS	1994-12-12	Paper
Realizability interpretation of generalized inductive definitions	1994-12-05	Paper
Realizability interpretation of coinductive definitions and program synthesis with streams	1994-11-29	Paper
Uniqueness of normal proofs of minimal formulas	1994-07-07	Paper
Program synthesis using realizability	1992-06-28	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Makoto Tatsuta