| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano |
Type checking and typability in domain-free lambda calculi.  |
Theor. Comput. Sci.  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta, Ferruccio Damiani |
Type Inference for Bimorphic Recursion |
GandALF |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta |
Static analysis of multi-staged programs via unstaging translation. |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta, Stefano Berardi |
Non-Commutative Infinitary Peano Arithmetic. |
CSL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Koji Nakazawa, Makoto Tatsuta |
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. |
Chicago J. Theor. Comput. Sci. |
2010 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano |
Inhabitation of polymorphic and existential types. |
Ann. Pure Appl. Logic |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta |
On isomorphisms of intersection types. |
ACM Trans. Comput. Log. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Makoto Tatsuta |
Internal Normalization, Compilation and Decompilation for System Fbh. |
FLOPS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen |
Completeness of Pointer Program Verification by Separation Logic. |
SEFM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Daisuke Kimura, Makoto Tatsuta |
Dual Calculus with Inductive and Coinductive Types. |
RTA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Non-Commutative First-Order Sequent Calculus. |
CSL |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Koji Nakazawa, Makoto Tatsuta |
Strong normalization of classical natural deduction with disjunctions. |
Ann. Pure Appl. Logic |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Types for Hereditary Head Normalizing Terms. |
FLOPS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Types for Hereditary Permutators. |
LICS |
2008 |
DBLP DOI BibTeX RDF |
hereditary permutator, infinite lambda-calculus, stream type, intersection type |
| 1 | Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano |
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. |
CSL |
2008 |
DBLP DOI BibTeX RDF |
domain-free type system, undecidability, existential type, CPS-translation |
| 1 | Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta |
On Isomorphisms of Intersection Types. |
CSL |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Mariangiola Dezani-Ciancaglini, Makoto Tatsuta |
A Behavioural Model for Klop's Calculus. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
The Maximum Length of Mu-Reduction in Lambda Mu-Calculus. |
RTA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Makoto Tatsuta |
Positive Arithmetic Without Exchange Is a Subclassical Logic. |
APLAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta, Mariangiola Dezani-Ciancaglini |
Normalisation is Insensible to lambda-Term Identity or Difference. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta, Grigori Mints |
A simple proof of second-order strong normalization with permutative conversions. |
Ann. Pure Appl. Logic |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Koji Nakazawa, Makoto Tatsuta |
Strong normalization proof with CPS-translation for second order classical natural deduction. |
J. Symb. Log. |
2003 |
DBLP BibTeX RDF |
|
| 1 | Koji Nakazawa, Makoto Tatsuta |
Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". |
J. Symb. Log. |
2003 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. |
MPC |
1998 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. |
LICS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Mitsuru Tada, Makoto Tatsuta |
The function ëa/mû\lfloor a/m\rfloor in sharply bounded arithmetic. |
Arch. Math. Log. |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Satoshi Kobayashi, Makoto Tatsuta |
Realizability Interpretation of Generalized Inductive Definitions. |
Theor. Comput. Sci. |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. |
Theor. Comput. Sci. |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Two Realizability Interpretations of Monotone Inductive Definitions. |
Int. J. Found. Comput. Sci. |
1994 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Uniqueness of Normal Proofs of Minimal Formulas. |
J. Symb. Log. |
1993 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams. |
FGCS |
1992 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Program Synthesis Using Realizability. |
Theor. Comput. Sci. |
1991 |
DBLP BibTeX RDF |
|
| 1 | Makoto Tatsuta |
Monotone Recursive Definition of Predicates and Its Realizability Interpretation. |
TACS |
1991 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")