Koji Nakazawa

Theor. Comput. Sci., 2024

Relative Completeness of Incorrectness Separation Logic.

[BibT_eX]

[DOI]

Yeonseok Lee

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2022

Z property for the shuffling calculus.

[BibT_eX]

[DOI]

Ken-etsu Fujita

Yuta Imagawa

Math. Struct. Comput. Sci., August, 2022

2021

Confluence Proofs of Lambda-Mu-Calculi by Z Theorem.

[BibT_eX]

[DOI]

Yuki Honda

Ken-etsu Fujita

Stud Logica, 2021

Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions.

[BibT_eX]

[DOI]

Kenji Saotome

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

Function Pointer Eliminator for C Programs.

[BibT_eX]

[DOI]

Mahmudul Faisal Al Ameen

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

2020

Restriction on Cut in Cyclic Proof System for Symbolic Heaps.

[BibT_eX]

[DOI]

Kenji Saotome

Proceedings of the Functional and Logic Programming - 15th International Symposium, 2020

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

2016

Compositional Z: Confluence Proofs for Permutative Conversion.

[BibT_eX]

[DOI]

Ken-etsu Fujita

Stud Logica, 2016

2015

Strong Reduction of Combinatory Calculus with Streams.

[BibT_eX]

[DOI]

Hiroto Naya

Stud Logica, 2015

2014

Confluence for classical logic through the distinction between values and computations.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

Reduction System for Extensional Lambda-mu Calculus.

[BibT_eX]

[DOI]

Tomoharu Nagai

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

2013

Monadic translation of classical sequent calculus.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2013

2012

Extensional Models of Untyped Lambda-mu Calculus

[BibT_eX]

[DOI]

Shin-ya Katsumata

Proceedings of the Proceedings Fourth Workshop on Classical Logic and Computation, 2012

2011

Type checking and typability in domain-free lambda calculi.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

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

2009

Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types.

[BibT_eX]

[DOI]

Yuki Kato

Proceedings of the Functional and Constraint Logic Programming, 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

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

An Isomorphism Between Cut-Elimination Procedure and Proof Reduction.

[BibT_eX]

[DOI]

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

2006

Strong normalization proofs by CPS-translations.

[BibT_eX]

[DOI]

Satoshi Ikeda

Inf. Process. Lett., 2006

2003

Confluency and strong normalizability of call-by-value lambda-µ-calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 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]