研究者詳細 - 中澤　巧爾

論文 - 中澤　巧爾

分割表示 48 件中 1 - 20 件目／全件表示 >>

Restriction on cut rule in cyclic-proof system for symbolic heaps 査読有り

Kenji Saotome, Koji Nakazawa, and Daisuke Kimura

Theoretical Computer Science 1019 巻 2024年12月

Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions 査読有り国際誌

Saotome K., Nakazawa K., Kimura D.

195 巻 2021年7月

記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：Leibniz International Proceedings in Informatics, LIPIcs

Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, Kimura et al. have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.

DOI： 10.4230/LIPIcs.FSCD.2021.11

Scopus

Compositional Z: Confluence proofs for permutative conversion 査読有り

Koji Nakazawa, Ken-etsu Fujita

Studia Logica 2016年5月

Monadic translation of classical sequent calculus 査読有り

J. Espírito Santo, R. Matthes, K. Nakazawa, L. Pinto

Mathematical Structures in Computer Science 23 巻 ( 6 ) 頁： 1111-1162 2013年12月

Type checking and typability in domain-free lambda calculi 査読有り

K. Nakazawa, M. Tatsuta, Y. Kameyama, H. Nakano

Theoretical Computer Science 412 巻 ( 44 ) 頁： 6193-6207 2011年10月

Strong normalization of classical natural deduction with disjunctions 査読有り

K. Nakazawa, M. Tatsuta

Annals of Pure and Applied Logic 153 巻 ( 1-3 ) 頁： 21-37 2008年4月

Strong normalization proof with CPS-translation for second order classical natural deduction 査読有り

K. Nakazawa, M. Tatsuta

Journal of Symbolic Logic 68 巻 ( 3 ) 頁： 851-859 2003年9月

Confluency and strong normalizability of call-by-value lambda-mu calculus 査読有り

K. Nakazawa

Theoretical Computer Science 290 巻頁： 429-463 2003年1月

Incorrectness Separation Logic with Arrays and Pointer Arithmetic

Yeonseok Lee and Koji nakazawa

arXiv 2025年3月

Cyclic-proof systems for symbolic heaps require cut formulas outside initial signatures 査読有り

Kenji Saotome and Koji Nakazawa

Journal of Information Processing 2025年

Relative completeness of incorrectness separation logic 査読有り

Yeonseok Lee and Koji nakazawa

The 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024), LNCS 2024年10月

再帰呼び出しを含む分離論理の部分正当性のための循環証明体系

佐藤拓海, 中澤巧爾

日本ソフトウェア科学会第41回大会講演論文集 2024年9月

分割可能なアクセス権限値をもつ並行分離論理における帰納的述語の拡張査読有り

佐藤拓海, 中澤巧爾, and 木村大輔

第26回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2024) 2024年3月

Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis

KIMURA Daisuke, TATSUTA Makoto, AL AMEEN Mahmudul Faisal, IKEBUCHI Mirai, NAKAZAWA Koji

コンピュータソフトウェア 41 巻 ( 1 ) 頁： 1_50 - 1_67 2024年1月

記述言語：日本語出版者・発行元：日本ソフトウェア科学会

<p>This paper gives an algorithm that solves the bi-abduction problem in symbolic-heap separation logic with arrays and lists. The logic is an assertion language of Hoare-style logic for program verification of pointer manipulating programs. The bi-abduction problem asks to find an additional assumption and an additional conclusion from a given assumption and a given conclusion such that the entailment becomes true. Bi-Abduction is indispensable for modular analysis and automatic verification with separation logic, since the condition at a call site that calls a function and the precondition of the called function are analyzed separately by modular analysis, and they both may contain spatial formulas of separation logic, and we have to guarantee they become the same by adding some spartial formulas to each of them. This paper shows the correctness of the bi-abduction algorithm with detailed proofs. A bi-abduction solver based on the algorithm has been implemented as a part of the authors' automatic program verifier, and experimental results of the bi-abduction solver with small inputs are also shown, which show the algorithm is usable.</p>

DOI： 10.11309/jssst.41.1_50

Scopus

CiNii Books

CiNii Research

その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I033331532

Decidable entailment checking for concurrent separation logic with fractional permissions

LEE Yeonseok, NAKAZAWA Koji

コンピュータソフトウェア 40 巻 ( 4 ) 頁： 4_67 - 4_86 2023年10月

記述言語：日本語出版者・発行元：日本ソフトウェア科学会

<p>We propose a subsystem of concurrent separation logic with fractional permissions introduced by Brotherston et al. Separation logic is an extension of Hoare logic that reasons about programs using shared mutable data. Separation logic has separating conjunction asserting that its subformulas hold for separated (disjoint) parts in the heap. Fractional permissions manage access permission of shared resources between concurrent threads. Brotherston et al. introduced an extension of concurrent separation logic with fractional permissions, but they still need to discuss the decidability of logic. The heart of this paper is restricting the formulas of the system to symbolic heaps. We present examples to illustrate that our system is appropriate to prove the entailment for data structures, such as list segments with cycles. We eliminate permissions by normalization, and therefore we can reduce the entailment checking problem to the existing decidable entailment checking.</p>

DOI： 10.11309/jssst.40.4_67

Scopus

CiNii Research

Z property for the shuffling calculus

Nakazawa, K; Fujita, KE; Imagawa, Y

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 32 巻 ( 7 ) 頁： 1015 - 1027 2022年8月

Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions (Theory and Applications of Proof and Computation)

Kimura Daisuke, Nakazawa Koji, Saotome Kenji

RIMS Kokyuroku 2228 巻頁： 59 - 72 2022年8月

記述言語：英語

Cyclic proof systems are extensions of the sequent-calculus style proof systems for logics with inductively defined predicates. In cyclic proof systems, inductive reasoning is realized as cyclic structures in proof trees. It has been already known that the cut-elimination property does not hold for the cyclic proof systems of some logics such as the first-order predicate logic and the separation logic. In this paper, we consider the cyclic proof systems with inductively defined propositions (that is, nullary predicates), and prove that the cut-elimination holds for the propositional logic, and it does not hold for the bunched logic.

CiNii Research

合流性とZ性について (証明と計算の理論と応用)

赤坂陸来, 藤田憲悦, 中澤巧爾

数理解析研究所講究録 2228 巻頁： 30 - 40 2022年8月

Biabduction for separation logic with arrays and lists 査読有り

Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Mirai Ikebuchi, and Koji Nakazawa

2022年3月

Confluence Proofs of Lambda-Mu-Calculi by Z Theorem 査読有り

Honda Yuki, Nakazawa Koji, Fujita Ken-Etsu

STUDIA LOGICA 109 巻 ( 5 ) 頁： 917 - 936 2021年10月

記述言語：日本語掲載種別：研究論文（学術雑誌）出版者・発行元：Studia Logica

This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s λμ-calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the λμ-calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional Z theorem can be applied to prove confluence of the call-by-name and the call-by-value λμ-calculi with both simplification rules, the renaming and the μη-rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants.

DOI： 10.1007/s11225-020-09931-0

Web of Science

Scopus

　前のページ - 次のページ　

<中澤 巧爾>

論文 - 中澤 巧爾

<中澤　巧爾>

論文 - 中澤　巧爾