BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Brazil
1 × Italy
1 × Norway
1 × Portugal
1 × The Netherlands
1 × Vietnam
2 × Japan
3 × France
4 × USA
Collaborated with:
∅ S.Berardi W.Chin M.Dezani-Ciancaglini D.Kimura M.F.A.Ameen W.Choi B.Aktemur K.Yi R.D.Cosmo E.Giovannetti K.Nakazawa Y.Kameyama H.Nakano Q.L.Le J.S.0001
Talks about:
type (6) program (4) logic (4) calculus (3) complet (3) induct (3) separ (3) hereditari (2) arithmet (2) normal (2)

Person: Makoto Tatsuta

DBLP DBLP: Tatsuta:Makoto

Contributed to:

SEFM 20142014
TLCA 20132013
CSL 20112011
POPL 20112011
FLOPS 20102010
CSL 20092009
RTA 20092009
SEFM 20092009
CSL 20082008
FLOPS 20082008
LICS 20082008
RTA 20072007
TLCA 20072007
LICS 20062006
LICS 19981998
CAV (2) 20172017

Wrote 17 papers:

SEFM-2014-TatsutaC #induction #logic #verification
Completeness of Separation Logic with Inductive Definitions for Program Verification (MT, WNC), pp. 20–34.
TLCA-2013-BerardiT #backtracking #game studies #logic #semantics #subclass
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics (SB, MT), pp. 61–76.
CSL-2011-TatsutaB #commutative
Non-Commutative Infinitary Peano Arithmetic (MT, SB), pp. 538–552.
POPL-2011-ChoiAYT #multi #source code #static analysis
Static analysis of multi-staged programs via unstaging translation (WC, BA, KY, MT), pp. 81–92.
FLOPS-2010-BerardiT #compilation #decompiler #normalisation
Internal Normalization, Compilation and Decompilation for System Fbh (SB, MT), pp. 207–223.
CSL-2009-Tatsuta #calculus #commutative #first-order
Non-Commutative First-Order Sequent Calculus (MT), pp. 470–484.
RTA-2009-KimuraT #calculus #induction
Dual Calculus with Inductive and Coinductive Types (DK, MT), pp. 224–238.
SEFM-2009-TatsutaCA #logic #pointer #verification
Completeness of Pointer Program Verification by Separation Logic (MT, WNC, MFAA), pp. 179–188.
CSL-2008-Dezani-CiancagliniCGT #morphism #on the
On Isomorphisms of Intersection Types (MDC, RDC, EG, MT), pp. 461–477.
CSL-2008-NakazawaTKN #λ-calculus
Undecidability of Type-Checking in Domain-Free Typed λ-Calculi with Existence (KN, MT, YK, HN), pp. 478–492.
FLOPS-2008-Tatsuta #normalisation
Types for Hereditary Head Normalizing Terms (MT), pp. 195–209.
LICS-2008-Tatsuta
Types for Hereditary Permutators (MT), pp. 83–92.
RTA-2007-Tatsuta #λ-calculus #μ-calculus
The Maximum Length of μ-Reduction in λμ-Calculus (MT), pp. 359–373.
TLCA-2007-Tatsuta #higher-order #quantifier #set
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification (MT), pp. 366–380.
LICS-2006-TatsutaD #difference #normalisation
Normalisation is Insensible to λ-Term Identity or Difference (MT, MDC), pp. 327–338.
LICS-1998-Tatsuta #synthesis
Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis (MT), pp. 358–367.
CAV-2017-LeT0C #decidability #induction #logic
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic (QLL, MT, JS0, WNC), pp. 495–517.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.