研究者詳細 - 中澤　巧爾

論文 - 中澤　巧爾

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

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

Function Pointer Eliminator for C Programs 査読有り国際共著国際誌

Kimura, D; Al Ameen, MF; Tatsuta, M; Nakazawa, K

PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2021 13008 巻頁： 23 - 37 2021年

記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Verification of memory safety such as absence of null pointer dereferences and memory leaks in system software is important in practice. O’Hearn’s group proposed a new method of memory safety analysis/verification by modular abstract interpretation with separation logic and biabduction. To realize this method, one has to construct a call graph before the modular abstract interpretation. This paper aims to analyze/verify memory safety of system software written in C programming language by this method, and as the first step this paper provides a function pointer eliminator tool to eliminate function pointer calls in order to construct a call graph. The tool uses SVF for pointer analysis. First C programs are translated into LLVM programs by Clang and then SVF analyses the LLVM programs. The tool given in this paper finds correspondence between function pointer calls in C programs and those in LLVM programs, and transforms the C programs into C programs with the same functionality and without any function pointer calls. The experimental results for gzip, git, and OpenSSL using this function pointer eliminator are presented and they show that this tool is sufficiently efficient and precise for the purpose.

DOI： 10.1007/978-3-030-89051-3_2

Web of Science

Scopus

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

Kenji Saotome, Koji Nakazawa, Daisuke Kimura

The 15th International Symposium on Functional and Logic Programming (FLOPS 2020) 頁： . 2020年9月

古典論理に対する汎用的自然演繹の証明正規化査読有り

福井康介, 中澤巧爾, 石井沙織, 結縁祥治

第22回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2020) 頁： . 2020年3月

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic 査読有り

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno

37 巻 ( 1 ) 頁： 39-52 2020年2月

Spatial Factorization in Cyclic-Proof System for Separation Logic 査読有り

Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura

頁： . 2020年

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic 査読有り

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno

頁： . 2019年3月

Spatial Factorization in Cyclic-Proof System for Separation Logic 査読有り

Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura

頁： . 2019年3月

高階契約に対するトレース意味論の完全抽象性査読有り

井上鉄也, 中澤巧爾

第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)論文集頁： . 2018年3月

Z for call-by-value 査読有り

Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

6th International Workshop on Cofluence (IWC 2017), 頁： 57–61 2017年9月

帰納的述語定義を含む分離論理における循環証明による半自動証明

仲田壮佑, 中澤巧爾

日本ソフトウェア科学会第33回大会講演論文集頁： . 2016年9月

Church-Rosser theorem and compositional Z-property

Ken-etsu Fujita, Koji Nakazawa

頁： . 2016年9月

Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild 査読有り

Takeshi Tsukada, Koji Nakazawa

頁： . 2016年3月

Compositional Z: Confluence proofs for permutative conversion

K. Nakazawa, K. Fujita

頁： . 2015年9月

Strong reduction of combinatory logic with streams 査読有り

K. Nakazawa, H. Naya

Studia Logica 103 巻頁： 375-387 2015年4月

高階契約を持つプログラミング言語に対するトレース意味論査読有り

村井涼, 五十嵐淳, 中澤巧爾

第17回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2015) 頁： . 2015年3月

Reduction system for extensional lambda-mu calculus 査読有り

Koji Nakazawa and Tomoharu Nagai

Lecture Notes in Computer Science (RTA-TLCA 2014) 8560 巻頁： 340-363 2014年7月

Confluence for classical logic through the distinction between values and computation 査読有り

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

Electric Proceedings in Theoretical Computer Science (CL&C 2014) 164 巻頁： 63-77 2014年7月

Extensional models of untyped lambda-mu calculus 査読有り

Koji Nakazawa and Shin-ya Katsumata

Electric Proceedings in Theoretical Computer Science (CL&C 2012) 97 巻頁： 35-47 2012年10月

Combinators for streams

K. Nakazawa

頁： CD-ROM 2011年9月

Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems 査読有り

頁： Article 7 2010年

Type checking and inference are equivalent in lambda calculi with existential types 査読有り

Y. Kato, K. Nakazawa

Lecture Notes in Computer Science (WFLP 2009) 5979 巻頁： 96-110 2010年

Type checking and inference for polymorphic and existential types 査読有り

K. Nakazawa, M. Tatsuta

Conferences in Research and Practice in Information Technology Series 94 巻頁： . 2009年

Undecidability of type-checking in domain-free typed lambda-calculi with existence 査読有り

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

Lecture Notes in Computer Science (CSL 2008) 5213 巻頁： 478-492 2008年9月

An isomorphism between cut-elimination procedure and proof reduction 査読有り

K. Nakazawa

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4583 LNCS 巻頁： 336-350 2007年

Strong normalization proofs by CPS-translations 査読有り

S. Ikeda, K. Nakazawa

Information Processing Letters 99 巻 ( 4 ) 頁： 163-170 2006年8月

選言を含む自然演繹古典論理の強正規化性査読有り

中澤巧爾, 龍田真

第8回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2006), 頁： . 2006年

コントロールオペレータをもつ計算体系の強正規化可能性のCPS変換を用いた証明査読有り

池田聡, 中澤巧爾

第7回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2005), 171--186 頁： . 2005年

値呼びラムダ・ミュー計算の合流性と強正規化性

中澤巧爾

日本ソフトウェア科学会第17回大会講演論文集頁： CD-ROM 2000年9月

　前のページ - 次のページ　

<中澤 巧爾>

論文 - 中澤 巧爾

<中澤　巧爾>

論文 - 中澤　巧爾