Makoto Tatsuta

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2021

Decidability for Entailments of Symbolic Heaps with Arrays.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions.

[BibT_eX]

[DOI]

Yukihiro Masuoka

CoRR, 2021

Function Pointer Eliminator for C Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021

2019

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

Completeness and expressiveness of pointer program verification by separation logic.

[BibT_eX]

[DOI]

Inf. Comput., 2019

Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018

Completeness of Cyclic Proofs for Symbolic Heaps.

[BibT_eX]

[DOI]

CoRR, 2018

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs.

[BibT_eX]

[DOI]

Proceedings of the Coalgebraic Methods in Computer Science, 2018

2017

Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14).

[BibT_eX]

[DOI]

Marieke Huisman

Thomas Noll

NII Shonan Meet. Rep., 2017

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic.

[BibT_eX]

[DOI]

CoRR, 2017

Equivalence of inductive definitions and cyclic proofs under arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2017

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Micro-clustering by data polishing.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE International Conference on Big Data (IEEE BigData 2017), 2017

Decision Procedure for Entailment of Symbolic Heaps with Arrays.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016

Completeness for recursive procedures in separation logic.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2016

Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic.

[BibT_eX]

[DOI]

Quang Loc Le

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Micro-Clustering: Finding Small Clusters in Large Diversity.

[BibT_eX]

[DOI]

CoRR, 2015

Separation Logic with Monadic Inductive Definitions and Implicit Existentials.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

2014

Completeness of Separation Logic with Inductive Definitions for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

2013

Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2012

Internal models of system F for decompilation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

Verification of Substitution Theorem Using HOL.

[BibT_eX]

[DOI]

Takayuki Koai

Inf. Media Technol., 2012

2011

Type checking and typability in domain-free lambda calculi.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Type Inference for Bimorphic Recursion

[BibT_eX]

[DOI]

Ferruccio Damiani

Proceedings of Second International Symposium on Games, 2011

Static analysis of multi-staged programs via unstaging translation.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Non-Commutative Infinitary Peano Arithmetic.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Proceedings of the Computer Science Logic, 2011

2010

On isomorphisms of intersection types.

[BibT_eX]

[DOI]

Roberto Di Cosmo

Elio Giovannetti

ACM Trans. Comput. Log., 2010

Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 2010

Inhabitation of polymorphic and existential types.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2010

Internal Normalization, Compilation and Decompilation for System Fbh.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

2009

Completeness of Pointer Program Verification by Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009

Dual Calculus with Inductive and Coinductive Types.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

Non-Commutative First-Order Sequent Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

Type Checking and Inference for Polymorphic and Existential Types.

[BibT_eX]

[DOI]

Proceedings of the Theory of Computing 2009, 2009

2008

Strong normalization of classical natural deduction with disjunctions.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2008

Types for Hereditary Permutators.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Types for Hereditary Head Normalizing Terms.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

Simple Saturated Sets for Disjunction and Second-Order Existential Quantification.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

The Maximum Length of Mu-Reduction in Lambda Mu-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Positive Arithmetic Without Exchange Is a Subclassical Logic.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

A Behavioural Model for Klop's Calculus.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Logic, Models and Computer Science, 2006

Normalisation is Insensible to lambda-Term Identity or Difference.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

2005

A simple proof of second-order strong normalization with permutative conversions.

[BibT_eX]

[DOI]

Grigori Mints

Ann. Pure Appl. Log., 2005

2003

Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction".

[BibT_eX]

[DOI]

J. Symb. Log., 2003

Strong normalization proof with CPS-translation for second order classical natural deduction.

[BibT_eX]

[DOI]

J. Symb. Log., 2003

1998

Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 1998

Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

1997

The function ëa/mû\lfloor a/m\rfloor in sharply bounded arithmetic.

[BibT_eX]

[DOI]

Mitsuru Tada

Arch. Math. Log., 1997

1994

Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

Realizability Interpretation of Generalized Inductive Definitions.

[BibT_eX]

[DOI]

Satoshi Kobayashi

Theor. Comput. Sci., 1994

Two Realizability Interpretations of Monotone Inductive Definitions.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 1994

1993

Uniqueness of Normal Proofs of Minimal Formulas.

[BibT_eX]

[DOI]

J. Symb. Log., 1993

1991

Program Synthesis Using Realizability.

[BibT_eX]

Theor. Comput. Sci., 1991

Monotone Recursive Definition of Predicates and Its Realizability Interpretation.

[BibT_eX]

[DOI]