2024/02/22 更新

写真a

ナカザワ コウジ
中澤 巧爾
NAKAZAWA Koji
所属
大学院情報学研究科 情報システム学専攻 ソフトウェア論 准教授
大学院担当
大学院情報科学研究科
大学院情報学研究科
学部担当
工学部 電気電子・情報工学科
情報学部 コンピュータ科学科
職名
准教授

学位 1

  1. 博士(理学) ( 2002年11月   京都大学 ) 

経歴 4

  1. 名古屋大学   大学院情報学研究科 情報システム学専攻 ソフトウェア論   准教授

    2017年4月 - 現在

  2. 名古屋大学   大学院情報科学研究科   准教授

    2015年10月 - 2017年3月

      詳細を見る

    国名:日本国

  3. 京都大学大学院情報学研究科助教

    2007年4月 - 2015年9月

      詳細を見る

    国名:日本国

  4. 京都大学大学院情報学研究科助手

    2002年12月 - 2007年3月

      詳細を見る

    国名:日本国

学歴 2

  1. 京都大学   理学研究科   数学・数理解析

    2000年4月 - 2002年11月

      詳細を見る

    国名: 日本国

  2. 京都大学   理学部

    1994年4月 - 1998年3月

      詳細を見る

    国名: 日本国

所属学協会 3

  1. European Association for Theoretical Computer Science

  2. 日本数学会

  3. 日本ソフトウェア科学会

委員歴 1

  1. 日本ソフトウェア科学会プログラミング論研究会運営委員   運営委員  

    2017年4月 - 2021年3月   

      詳細を見る

    団体区分:学協会

受賞 4

  1. 研究論文賞

    2022年9月   日本ソフトウェア科学会  

  2. PPL2020論文賞

    2020年3月   日本ソフトウェア科学会プログラミング論研究会   古典論理に対する汎用的自然演繹の証明正規化

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

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  3. 高橋奨励賞

    2016年9月   日本ソフトウェア科学会  

     詳細を見る

    受賞国:日本国

  4. PPL2006 Best Paper Award

    2006年3月   日本ソフトウェア科学会プログラミング論研究会   選言を含む自然演繹古典論理の強正規化性

    中澤巧爾,龍田真

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

 

論文 42

  1. Bi-abduction in separation logic with arrays and lists for program analysis 査読有り 国際共著

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

    コンピュータ ソフトウェア   41 巻 ( 1 ) 頁: 50 - 67   2024年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:日本ソフトウェア科学会  

    <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>

  2. 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

  3. Cut-elimination for cyclic proof systems with inductively defined propositions

    Daisuke Kimura, Koji Nakazawa, Kenji Saotome

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

     詳細を見る

    担当区分:責任著者   記述言語:英語   掲載種別:研究論文(大学,研究機関等紀要)  

  4. 合流性とZ定理について

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

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

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(大学,研究機関等紀要)  

  5. Z property for the shuffling calculus

    Nakazawa Koji, Fujita Ken-etsu, Imagawa Yuta

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

     詳細を見る

    出版者・発行元:Mathematical Structures in Computer Science  

    This paper gives a new proof of confluence for Carraro and Guerrieri's call-by-value lambda calculus λ v σ with permutation rules. We adapt the compositional Z theorem to λ v σ.

    DOI: 10.1017/S0960129522000408

    Web of Science

    Scopus

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

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

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

     詳細を見る

    記述言語:日本語   出版者・発行元:京都大学数理解析研究所  

    CiNii Research

  7. 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

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

    Saotome K., Nakazawa K., Kimura D.

    Leibniz International Proceedings in Informatics, LIPIcs   195 巻   2021年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.4230/LIPIcs.FSCD.2021.11

    Scopus

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

    Kimura Daisuke, Al Ameen Mahmudul Faisal, Tatsuta Makoto, Nakazawa Koji

    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

  10. 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月

     詳細を見る

    記述言語:英語  

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

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

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

     詳細を見る

    記述言語:日本語  

  12. 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月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

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

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

        頁: .   2020年

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

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

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

        頁: .   2019年3月

     詳細を見る

    記述言語:英語  

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

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

        頁: .   2019年3月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

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

    井上 鉄也, 中澤 巧爾

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

     詳細を見る

    記述言語:日本語  

  17. Z for call-by-value 査読有り

    Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

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

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

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

    仲田 壮佑, 中澤 巧爾

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

     詳細を見る

    記述言語:日本語  

    DOI: .

  19. Church-Rosser theorem and compositional Z-property

    Ken-etsu Fujita, Koji Nakazawa

        頁: .   2016年9月

     詳細を見る

    記述言語:英語  

    DOI: .

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

    Koji Nakazawa, Ken-etsu Fujita

    Studia Logica     2016年5月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1007/s11225-016-9673-0

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

    Takeshi Tsukada, Koji Nakazawa

        頁: .   2016年3月

     詳細を見る

    記述言語:英語  

    DOI: .

  22. Compositional Z: Confluence proofs for permutative conversion

    K. Nakazawa, K. Fujita

        頁: .   2015年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

    DOI: .

  23. Strong reduction of combinatory logic with streams 査読有り

    K. Nakazawa, H. Naya

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

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1007/s11225-014-9570-3

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

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

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

     詳細を見る

    記述言語:日本語  

    DOI: .

  25. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

    DOI: 10.1007/978-3-319-08918-8_24

  26. 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月

     詳細を見る

    記述言語:英語  

    DOI: 10.4204/EPTCS.164.5

  27. 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月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1017/S0960129512000436

  28. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

    DOI: 10.4204/EPTCS.97.3

  29. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1016/j.tcs.2011.06.020

  30. Combinators for streams

    K. Nakazawa

        頁: CD-ROM   2011年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

    DOI: CD-ROM

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

        頁: Article 7   2010年

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  32. 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年

     詳細を見る

    記述言語:英語  

    DOI: 10.1007/978-3-642-11999-6_7

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

    K. Nakazawa, M. Tatsuta

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

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

  34. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語  

    DOI: 10.1007/978-3-540-87531-434

  35. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1016/j.apal.2008.01.003

  36. 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年

     詳細を見る

    記述言語:英語  

  37. Strong normalization proofs by CPS-translations 査読有り

    S. Ikeda, K. Nakazawa

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

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1016/j.ipl.2006.03.009

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

    中澤 巧爾, 龍田 真

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

     詳細を見る

    記述言語:日本語  

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

    池田 聡, 中澤 巧爾

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

     詳細を見る

    記述言語:日本語  

  40. 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月

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.2178/jsl/1067620196

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

    K. Nakazawa

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

     詳細を見る

    担当区分:筆頭著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1016/S0304-3975(01)00380-2

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

    中澤巧爾

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

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

    DOI: CD-ROM

▼全件表示

書籍等出版物 2

  1. プログラミング言語の形式的意味論入門

    Winskel Glynn, 勝股 審也, 中澤 巧爾, 西村 進, 前田 敦司, 末永 幸平( 担当: 共訳 ,  範囲: 10〜11章)

    丸善出版  2023年  ( ISBN:9784621307632

     詳細を見る

    担当ページ:183-242   記述言語:日本語 著書種別:学術書

    CiNii Books

  2. 理論計算機科学事典

    徳山 豪,小林 直樹(総編集)( 担当: 分担執筆 ,  範囲: 8.2章)

    2022年1月 

     詳細を見る

    総ページ数:816   記述言語:日本語 著書種別:事典・辞書

講演・口頭発表等 42

  1. Z定理のモジュール性

    女屋優貴,藤田憲悦,中澤巧爾

    RIMS共同研究「証明論と計算論の最前線」  2023年12月11日 

     詳細を見る

    開催年月日: 2023年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:京都大学   国名:日本国  

  2. 命題論理に対する無限証明体系と循環証明体系の証明能力同等性

    堀弘昌, 中澤巧爾, 龍田真

    日本数学会秋季総合分科会  2022年9月  日本数学会

     詳細を見る

    開催年月日: 2022年9月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:北海道大学   国名:日本国  

  3. 不動点演算子を持つ命題論理の循環証明体系

    中澤巧爾, 堀弘昌, 龍田真

    SLACS 2022  2022年9月 

     詳細を見る

    開催年月日: 2022年9月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:東邦大学   国名:日本国  

  4. Decidable entailment checking for concurrent separation logic with fractional permissions 国際共著

    Yeonseok Lee, Koji Nakazawa

    2022年8月31日 

     詳細を見る

    開催年月日: 2022年8月 - 2022年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  5. Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions 国際共著

    2022年3月6日 

     詳細を見る

    開催年月日: 2022年3月

    記述言語:英語   会議種別:ポスター発表  

    国名:日本国  

  6. 無限証明体系と循環証明体系の証明能力同等性 国際共著

    堀弘昌,中澤巧爾,龍田真

    第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022)  2022年3月7日  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2022年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:オンライン   国名:日本国  

  7. 制限された帰納的述語を含む分離論理の完全な循環証明体系 国際共著

    石井沙織,中澤巧爾

    第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022)  2022年3月7日  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2022年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:オンライン   国名:日本国  

  8. 帰納的命題を含む循環証明体系のカット除去

    中澤巧爾,早乙女献自,木村大輔

    RIMS共同研究「証明と計算の理論と応用」  2021年12月20日 

     詳細を見る

    開催年月日: 2021年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:京都大学   国名:日本国  

  9. 合流性とZ定理について

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

    RIMS共同研究「証明と計算の理論と応用」  2021年12月20日 

     詳細を見る

    開催年月日: 2021年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:京都大学   国名:日本国  

  10. 分離論理 招待有り

    中澤 巧爾

    2021年度数学基礎論サマースクール(古典論理に限らない論理)  2021年9月  日本数学会

     詳細を見る

    開催年月日: 2021年9月

    記述言語:日本語   会議種別:公開講演,セミナー,チュートリアル,講習,講義等  

    開催地:オンライン   国名:日本国  

  11. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions 国際会議

    Koji Nakazawa, Kenji Saotome, Daisuke Kimura

    Forth Workshop on Mathematical Logic and its Applications (MLA 2021)  2021年3月 

     詳細を見る

    開催年月日: 2021年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:日本国  

  12. 分離論理におけるエンテイルメント判定問題の決定不能性

    飯田 晟樹,早乙女 献自,中澤 巧爾

    第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021)  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2021年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:オンライン   国名:日本国  

  13. 分離論理の循環証明体系における帰納的述語の制限とカット除去

    早乙女 献自, 中澤 巧爾

    SLACS 2020  2020年12月 

     詳細を見る

    開催年月日: 2020年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:オンライン   国名:日本国  

  14. 書換え系の変換を用いたZ性の証明

    本多 雄樹, 中澤 巧爾

    SLACS 2020  2020年12月 

     詳細を見る

    開催年月日: 2020年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:オンライン   国名:日本国  

  15. 書換え系の変換を用いたZ性の証明

    本多 雄樹,中澤 巧爾

    日本ソフトウェア科学会第 37 回大会  2020年9月  日本ソフトウェア科学会

     詳細を見る

    開催年月日: 2020年9月

    記述言語:日本語   会議種別:口頭発表(一般)  

    開催地:オンライン   国名:日本国  

  16. Proof Normalization for Classical Truth-Table Natural Deduction

    Kosuke Fukui, Saori Ishii, Koji Nakazawa, and Takeshi Tsukada

    2020年9月 

     詳細を見る

    開催年月日: 2020年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  17. 分離論理におけるエンテイルメント証明器の入力に対する制限の緩和

    青木 洸佑, 中澤 巧爾, 木村 大輔

    第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020)  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2020年2月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:オンライン   国名:日本国  

  18. 分離論理における記号ヒープのための循環証明体系におけるカットの制限について

    早乙女 献自, 中澤 巧爾, 木村 大輔

    第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020)  日本ソフトウェア科学会プログラミング論研究会

     詳細を見る

    開催年月日: 2020年2月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:オンライン   国名:日本国  

  19. On restricted cut-elimination for cyclic proof system for separation logic

     詳細を見る

    開催年月日: 2019年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

  20. Confluence proof of lambda-mu-calculus by Z thorem

     詳細を見る

    開催年月日: 2019年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

  21. Proof normalization for classical truth-table natural deduction

     詳細を見る

    開催年月日: 2019年12月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

  22. On cut elimination in cyclic-proof systems 国際会議

    Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome

    The 51st TRS Meeting 

     詳細を見る

    開催年月日: 2019年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  23. Confluence Proof of lambda-mu-Calculus by Z Theorem 国際会議

    Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita

    The 51st TRS Meeting 

     詳細を見る

    開催年月日: 2019年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  24. プログラムの正しさを証明する ---分離論理入門--- 招待有り

    中澤 巧爾

    日本数学会2019年度年会 

     詳細を見る

    開催年月日: 2019年3月

    記述言語:日本語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

  25. Z定理を用いたラムダ・ミュー計算の合流性証明

    本多 雄樹, 中澤 巧爾

    第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) 

     詳細を見る

    開催年月日: 2019年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:花巻市   国名:日本国  

  26. 循環証明体系における準カット除去可能性について

    早乙女 献自, 中澤 巧爾

    第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) 

     詳細を見る

    開催年月日: 2019年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:花巻市   国名:日本国  

  27. On Cut-Elimination in Cyclic Proof Systems 国際会議

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

    16th Asian Symposium on Programming Languages and Systems (APLAS 2018) 

     詳細を見る

    開催年月日: 2018年12月

    記述言語:英語   会議種別:ポスター発表  

    開催地:Wellington   国名:ニュージーランド  

  28. On Cut-Elimination in Cyclic Proof Systems 国際会議

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

    Workshop on New Ideas and Emerging Results (NIER 2019) 

     詳細を見る

    開催年月日: 2018年12月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:ニュージーランド  

  29. Cyclic Theorem Prover for Separation Logic by Magic Wand. 国際会議

    Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura

    1st Workshop on Automated Deduction for Separation Logics (ADSL 2018) 

     詳細を見る

    開催年月日: 2018年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Oxford, UK   国名:グレートブリテン・北アイルランド連合王国(英国)  

  30. Complete Axiom System of Cluster Algebra 国際会議

    Kousuke Fukui and Koji Nakazawa

    7th International Workshop on Confluence (IWC 2018) 

     詳細を見る

    開催年月日: 2018年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Oxford, UK   国名:グレートブリテン・北アイルランド連合王国(英国)  

  31. 帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出

    仲田 壮佑, 中澤 巧爾

    第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018) 

     詳細を見る

    開催年月日: 2018年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:米子市   国名:日本国  

  32. Completeness of Cyclic Proofs for Symbolic Heaps. 国際会議

    Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura

    Second Workshop on Mathematical Logic and its Applications (MLA 2018) 

     詳細を見る

    開催年月日: 2018年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  33. Complete cyclic-proof system for separation logic with general inductive predicates 招待有り 国際会議

     詳細を見る

    開催年月日: 2017年10月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

  34. Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions 国際会議

    Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa

    2nd Workshop on New and Emerging Results in Programming Languages and Systems 

     詳細を見る

    開催年月日: 2016年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Halong Bay, Vietnam   国名:ベトナム社会主義共和国  

  35. Characterizing trees for lambda-mu terms 国際会議

    Koji Nakazawa

    8th International Workshop on Higher-Order Rewriting (HOR 2016) 

     詳細を見る

    開催年月日: 2016年6月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Porto, Portugal   国名:ポルトガル共和国  

  36. A denotational semantics of a probabilistic stream-processing language 国際会議

    Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa

    Workshop on probabilistic programming semantics (PPS 2016) 

     詳細を見る

    開催年月日: 2016年1月

    記述言語:英語   会議種別:ポスター発表  

    開催地:Florida, US   国名:アメリカ合衆国  

  37. Lambda calculi and confluence from A to Z 国際会議

    K. Nakazawa

    4th International Workshop on Confluence (IWC 2015) 

     詳細を見る

    開催年月日: 2015年8月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

  38. 置換簡約を含むラムダ計算の合流性

    中澤巧爾, 藤田憲悦

    第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) 

     詳細を見る

    開催年月日: 2015年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:松山   国名:日本国  

  39. 京都大学 teen racketeer 養成コース

    五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平

    第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) 

     詳細を見る

    開催年月日: 2015年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:松山   国名:日本国  

  40. Extensional models of typed lambda-mu calculus 国際会議

    K. Nakazawa

    The Fifth International Workshop on Classical Logic and Computation (CL&C'14) 

     詳細を見る

    開催年月日: 2014年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  41. Extensional model of Lambda-mu calculus

     詳細を見る

    開催年月日: 2013年9月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

  42. Continuations and classical logic: using continuations as a tool for classical logic 国際会議

    K. Nakazawa

    Continuation Workshop (CW2011) 

     詳細を見る

    開催年月日: 2011年9月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

▼全件表示

共同研究・競争的資金等の研究課題 10

  1. 分離論理における帰納的述語とエンテイルメント判定問題

    研究課題番号:21FP01  2021年4月 - 2022年3月

    公募型共同研究 

    中澤 巧爾,龍田 真,木村 大輔,Mahmudul Faisal Al Ameen

      詳細を見る

    担当区分:研究代表者  資金種別:競争的資金

    配分額:190000円

  2. 制限された帰納的述語をもつ循環証明体系のカット除去可能性

    研究課題番号:20FP03  2020年4月 - 2021年3月

    公募型共同研究 

    中澤 巧爾,龍田 真

      詳細を見る

    担当区分:研究代表者  資金種別:競争的資金

    配分額:376000円

  3. ストリーム計算のための型システム

    2013年4月 - 2014年3月

    国内共同研究 

  4. ストリームを扱う計算体系とそのモデル

    2012年4月 - 2013年3月

    国内共同研究 

  5. 暗黙的に型付けされた多相型・存在型を含むラムダ計算

    2011年4月 - 2012年3月

    国内共同研究 

  6. 型推論が決定可能な存在型を含む型付ラムダ計算

    2010年4月 - 2011年3月

    国内共同研究 

  7. 多相型・存在型を含む型付きラムダ計算における型検査問題

    2009年4月 - 2010年3月

    国内共同研究 

  8. 簡単共通部分型理論とラムダ計算のモデルについて

    2008年4月 - 2009年3月

    国内共同研究 

  9. 古典シーケント計算の計算論的意味

    2007年4月 - 2008年3月

    国内共同研究 

  10. 古典論理に対応する型理論

    2006年4月 - 2007年3月

    国内共同研究 

▼全件表示

科研費 16

  1. 循環証明体系におけるカット除去定理とカット規則の制限

    研究課題/研究課題番号:22K11901  2022年4月 - 2026年3月

    日本学術振興会  科学研究費助成事業 基盤研究(C)  基盤研究(C)

    中澤 巧爾, 木村 大輔, 木村 大輔

      詳細を見る

    担当区分:研究代表者 

    配分額:4030000円 ( 直接経費:3100000円 、 間接経費:930000円 )

    循環証明体系は,帰納法に相当する原理を証明の循環構造によって表現する証明体系であり,自動証明との相性が良いことが知られている.本研究では,証明体系の重要な性質である「カット除去可能性」に注目する.カット規則は推論規則の一つであるが,カット規則の適用は自動証明においては不都合である.そのため,カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが,多くの循環証明体系ではカット除去可能性が成立しないことが分かっている.本研究では,論理に制限を課した上でのカット除去可能性や,自動証明の邪魔をしない程度までカット規則を制限できないか,などを明らかにする.

  2. データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法

    研究課題/研究課題番号:21H03415  2021年4月 - 2026年3月

    日本学術振興会  科学研究費助成事業 基盤研究(B)  基盤研究(B)

    結縁 祥治, 小川 瑞史, 今井 敬吾, 関 浩之, 中澤 巧爾, 小川 瑞史, 今井 敬吾, 関 浩之, 中澤 巧爾

      詳細を見る

    担当区分:研究分担者 

    実データを含むサブシステムの振舞いを拡張有限状態機械(EFSM)としてモデル化し振舞い合成と分解について、通信プロセスの形式化に基づいて振舞いの頑健性として振舞いの安定性を導く設計手法を確立する。この研究においては、システムの分解と合成の検証における抽象モデルと実現モデルとの関係に着目して研究を行う。それぞれのサブシステム自体が持つサンプリングやクロックドリフトに基づく誤差が全体システムの安定性を損なわないことを保証する。合成、分解においては、全体の設計情報に基づいて相互に可能な振舞いを自動的に学習して、効率的で現実的な検証およびテストのためのを設計モデルを導く。

  3. 分離論理を用いたソフトウェア検証の発展

    研究課題/研究課題番号:21H03421  2021年4月 - 2024年3月

    日本学術振興会  科学研究費助成事業 基盤研究(B)  基盤研究(B)

    龍田 真, 中澤 巧爾, 木村 大輔, 中澤 巧爾, 木村 大輔

      詳細を見る

    担当区分:研究分担者 

    ソフトウェア検証理論として近年よい理論(オハーン理論)が提案され理論的にも実用的にも成功しているが, 精度がまだ不十分である. 本研究の大目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することである. 本研究の目的は, オハーン理論に一般的述語, 配列, 算術を追加した論理体系に対して, 関数の再帰呼出しを追加し, 再帰データを追加し, また, 関数ポインタ呼出しを追加し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. この実装システムを用いてOpenSSLおよびgitのCコードのメモリー安全性を検証する.

  4. 循環証明体系の証明論的分析

    研究課題/研究課題番号:18K11161  2018年4月 - 2021年3月

    日本学術振興会  科学研究費助成事業 基盤研究(C)  基盤研究(C)

    中澤 巧爾, 木村 大輔

      詳細を見る

    本研究では,帰納的に定義された述語を含む論理式に対する証明体系である循環証明体系に注目し,その基本性質であるカット除去可能性などの証明論的性質を調べた.主な成果は以下のとおりである.(1) プログラム検証に利用されている分離論理において,シンボリックヒープと呼ばれる論理式のクラスに対する循環証明体系ではカット除去ができない例があることを示した.(2) この循環証明体系において,カットをある種の部分論理式にまで制限しても証明能力が真に異なることを示した.(3) 分離論理の基盤論理であるbunched logicに対する循環証明体系でもカット除去ができない例があることを示した.

  5. 実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル

    研究課題/研究課題番号:17H01722  2017年4月 - 2021年3月

    日本学術振興会  科学研究費助成事業 基盤研究(B)  基盤研究(B)

    結縁 祥治, 西田 直樹, 関 浩之, 中澤 巧爾

      詳細を見る

    本研究の目的は、並行性をもつソフトウェアにおいて、逆計算のメカニズムを応用して新たな解析手法を与えることである。近年の並行性を持つソフトウェアの振舞いにおいては、同時に実行されるプログラムの振舞いは非決定的であり、どのように相互作用を行ったかということを逆にたどることはプログラムの動的解析にとって非常に重要な情報となる。
    この観点において、本研究では、並行性を持つソフトウェアの振舞いモデルの研究を行い、応用技術として、デバッグを目的とした並行性をもつプログラムの逆方向の動的解析手法および関連したプログラム解析技法(情報圧縮、実時間計算、並行プログラムの型づけ)について研究を行った。

  6. 現代的なプログラミング言語のための漸進的型システムの理論

    研究課題/研究課題番号:17H01723  2017年4月 - 2021年3月

    日本学術振興会  科学研究費助成事業 基盤研究(B)  基盤研究(B)

    五十嵐 淳, 馬谷 誠二, 中澤 巧爾, 海野 広志

      詳細を見る

    漸進的型付けはひとつのプログラム中に静的型付けされる部分と動的型付けされる部分を共存させるための、プログラミング言語技術である.これを先進的なプログラミング言語に適用するための理論的基盤の研究を行った.主な成果は、多相性、セッション型、篩型、非決定性、ML型推論、交差型といった先進的なプログラミング言語機構へ漸進的型付けを導入した計算体系を与え、その性質(型安全性など)を証明した.さらに、漸進的型付けの実装技術として提案されている空間効率のよいコアーション計算を改良し、コアーション渡し形式を経由するコンパイル方法を提案し、実際に実装・評価を行い、その効果を確認した.

  7. 計算における無限概念と古典論理

    2015年4月 - 2018年3月

    科学研究費補助金  基盤研究(C)

    中澤巧爾

      詳細を見る

    担当区分:研究代表者 

  8. ソフトウェア契約に基づく高階型付プログラムの理論

    2013年4月 - 2016年3月

    科学研究費補助金  基盤研究(A)

    五十嵐淳

      詳細を見る

    担当区分:研究分担者 

  9. ストリーム計算のための計算モデル

    2012年4月 - 2015年3月

    科学研究費補助金  若手研究(B)

    中澤巧爾

      詳細を見る

    担当区分:研究代表者 

  10. バグのないソフトウェア構築環境に関する研究の新展開

    2010年4月 - 2013年3月

    科学研究費補助金  基盤研究(B)

    佐藤雅彦

      詳細を見る

    担当区分:研究分担者 

  11. 二階存在量化子をもつ計算体系

    2009年4月 - 2012年3月

    科学研究費補助金  若手研究(B)

    中澤巧爾

      詳細を見る

    担当区分:研究代表者 

  12. 計算と論理の融合によるバグのないソフトウェア構築環境に関する研究

    2007年4月 - 2010年3月

    科学研究費補助金  基盤研究(B)

    佐藤雅彦

      詳細を見る

    担当区分:研究分担者 

  13. 古典論理の構文論的双対性とその計算論的意味

    2006年4月 - 2009年3月

    科学研究費補助金  若手研究(B)

    中澤巧爾

      詳細を見る

    担当区分:研究代表者 

  14. 安全・安心な環境適応型ソフトウェアの基礎理論に関する研究

    2006年4月 - 2007年3月

    科学研究費補助金  特定領域研究

    五十嵐淳

      詳細を見る

    担当区分:研究分担者 

  15. 古典論理に基づく非決定的計算体系

    2004年4月 - 2006年3月

    科学研究費補助金  若手研究(B)

    中澤巧爾

      詳細を見る

    担当区分:研究代表者 

  16. 変数の動的束縛機構をもつ新しいソフトウェアの理論的研究

    2004年4月 - 2006年3月

    科学研究費補助金  特定領域研究

    佐藤雅彦

      詳細を見る

    担当区分:研究分担者 

▼全件表示

 

担当経験のある科目 (本学) 3

  1. 基礎セミナー

    2016

     詳細を見る

    様々なパラドックスを紹介し、議論することによって論理的思考や科学的内容の発表、議論の方法を学ぶ。

  2. プログラミング基礎及び演習

    2016

     詳細を見る

    C言語とJavaによるプログラミングの基礎。

  3. プログラミング基礎及び演習

    2015

     詳細を見る

    C言語とJavaによるプログラミングの基礎。

担当経験のある科目 (本学以外) 2

  1. 基礎セミナー

    名古屋大学)

  2. プログラミング基礎及び演習

    名古屋大学)

 

学術貢献活動 2

  1. FLOPS 2020 program committee member 国際学術貢献

    役割:査読

    2020年9月

     詳細を見る

    種別:学会・研究会等 

  2. 日本ソフトウェア科学会プログラミング論研究会運営委員

    役割:企画立案・運営等

    日本ソフトウェア科学会プログラミング論研究会  2017年4月 - 2021年3月

     詳細を見る

    種別:学会・研究会等