5 citations · 5 across the 4 of their papers we have counts for
4 papers
Cut elimination for propositional cyclic proof systems with fixed-point operators
Hiromasa Hori, Koji Nakazawa, Makoto Tatsuta
Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corres…
Completeness of Cyclic Proofs for Symbolic Heaps
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic p…
Confluence for classical logic through the distinction between values and computations
José Espírito Santo, Ralph Matthes, Koji Nakazawa +1
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-e…
Extensional Models of Untyped Lambda-mu Calculus
Koji Nakazawa, Shin-ya Katsumata
This paper proposes new mathematical models of the untyped Lambda-mu calculus. One is called the stream model, which is an extension of the lambda model, in which each term is inte…