2024/09/18 更新

写真a

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

学位 1

  1. 博士（理学） （ 2002年11月   京都大学 ） 

学位の先頭へ▲

経歴 5

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

    2017年4月 - 現在

  2. 名古屋大学

    2015年10月 - 現在

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

    2015年10月 - 2017年3月

    　 詳細を見る

    国名：日本国

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

    2007年4月 - 2015年9月

    　 詳細を見る

    国名：日本国

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

    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月   日本ソフトウェア科学会プログラミング論研究会   選言を含む自然演繹古典論理の強正規化性

    中澤巧爾，龍田真

    　詳細を見る

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

受賞の先頭へ▲
 

論文 45

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

    Kenji Saotome, Koji Nakazawa, and Daisuke Kimura

    Theoretical Computer Science   1019 巻   2024年12月

    　詳細を見る

    担当区分：最終著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1016/j.tcs.2024.114854

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

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

    Koji Nakazawa, Ken-etsu Fujita

    Studia Logica     2016年5月

    　詳細を見る

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

    DOI： 10.1007/s11225-016-9673-0

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

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

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

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

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

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

    　詳細を見る

    担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

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

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

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

    　詳細を見る

    担当区分：最終著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

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

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

  13. Z property for the shuffling calculus

    Nakazawa, K; Fujita, KE; Imagawa, Y

    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

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

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

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

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

    　詳細を見る

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

    CiNii Research

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

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

        2022年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

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

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

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

    　詳細を見る

    記述言語：英語  

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

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

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

    　詳細を見る

    記述言語：日本語  

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

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

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

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

        頁： .   2020年

    　詳細を見る

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

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

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

        頁： .   2019年3月

    　詳細を見る

    記述言語：英語  

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

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

        頁： .   2019年3月

    　詳細を見る

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

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

    井上 鉄也, 中澤 巧爾

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

    　詳細を見る

    記述言語：日本語  

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

    Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

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

    　詳細を見る

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

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

    仲田 壮佑, 中澤 巧爾

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

    　詳細を見る

    記述言語：日本語  

    DOI： .

  28. Church-Rosser theorem and compositional Z-property

    Ken-etsu Fujita, Koji Nakazawa

        頁： .   2016年9月

    　詳細を見る

    記述言語：英語  

    DOI： .

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

    Takeshi Tsukada, Koji Nakazawa

        頁： .   2016年3月

    　詳細を見る

    記述言語：英語  

    DOI： .

  30. Compositional Z: Confluence proofs for permutative conversion

    K. Nakazawa, K. Fujita

        頁： .   2015年9月

    　詳細を見る

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

    DOI： .

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

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

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

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

    　詳細を見る

    記述言語：日本語  

    DOI： .

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

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

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

  36. Combinators for streams

    K. Nakazawa

        頁： CD-ROM   2011年9月

    　詳細を見る

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

    DOI： CD-ROM

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

        頁： Article 7   2010年

    　詳細を見る

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

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

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

    K. Nakazawa, M. Tatsuta

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

    　詳細を見る

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

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

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

    　詳細を見る

    記述言語：英語  

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

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

    中澤 巧爾, 龍田 真

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

    　詳細を見る

    記述言語：日本語  

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

    池田 聡, 中澤 巧爾

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

    　詳細を見る

    記述言語：日本語  

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

    中澤巧爾

    日本ソフトウェア科学会第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   記述言語：日本語 著書種別：事典・辞書

書籍等出版物の先頭へ▲

講演・口頭発表等 45

  1. Relative completeness of incorrectness separation logic

    Koji Nakazawa and Yeonseok Lee

    2024年8月 

    　詳細を見る

    開催年月日： 2024年8月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

  2. Toward completeness of incorrectness separation logic

    Lee Yeonseok and Koji Nakazawa

    2024年3月 

    　詳細を見る

    開催年月日： 2024年3月

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

    国名：日本国  

  3. 不動点演算子を持つ命題論理に対する循環証明体系のカット無し完全性

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

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

    　詳細を見る

    開催年月日： 2024年3月

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

    開催地：新潟   国名：日本国  

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

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

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

    　詳細を見る

    開催年月日： 2023年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

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

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

    　詳細を見る

    開催年月日： 2022年9月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

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

    SLACS 2022  2022年9月 

    　詳細を見る

    開催年月日： 2022年9月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

    Yeonseok Lee, Koji Nakazawa

    2022年8月31日 

    　詳細を見る

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

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    2022年3月6日 

    　詳細を見る

    開催年月日： 2022年3月

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

    国名：日本国  

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

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

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

    　詳細を見る

    開催年月日： 2022年3月

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

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

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

    石井沙織，中澤巧爾

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

    　詳細を見る

    開催年月日： 2022年3月

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

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

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

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

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

    　詳細を見る

    開催年月日： 2021年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

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

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

    　詳細を見る

    開催年月日： 2021年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

  13. 分離論理 招待有り

    中澤 巧爾

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

    　詳細を見る

    開催年月日： 2021年9月

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

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

  14. 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   国名：日本国  

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

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

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

    　詳細を見る

    開催年月日： 2021年3月

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

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

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

    早乙女 献自, 中澤 巧爾

    SLACS 2020  2020年12月 

    　詳細を見る

    開催年月日： 2020年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

    本多 雄樹, 中澤 巧爾

    SLACS 2020  2020年12月 

    　詳細を見る

    開催年月日： 2020年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

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

    本多 雄樹，中澤 巧爾

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

    　詳細を見る

    開催年月日： 2020年9月

    記述言語：日本語   会議種別：口頭発表（一般）  

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

  19. Proof Normalization for Classical Truth-Table Natural Deduction

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

    2020年9月 

    　詳細を見る

    開催年月日： 2020年9月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

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

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

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

    　詳細を見る

    開催年月日： 2020年2月

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

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

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

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

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

    　詳細を見る

    開催年月日： 2020年2月

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

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

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

    　詳細を見る

    開催年月日： 2019年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    　詳細を見る

    開催年月日： 2019年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

  24. Proof normalization for classical truth-table natural deduction

    　詳細を見る

    開催年月日： 2019年12月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

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

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

    The 51st TRS Meeting 

    　詳細を見る

    開催年月日： 2019年9月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita

    The 51st TRS Meeting 

    　詳細を見る

    開催年月日： 2019年9月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    中澤 巧爾

    日本数学会2019年度年会 

    　詳細を見る

    開催年月日： 2019年3月

    記述言語：日本語   会議種別：口頭発表（招待・特別）  

    国名：日本国  

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

    本多 雄樹, 中澤 巧爾

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

    　詳細を見る

    開催年月日： 2019年3月

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

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

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

    早乙女 献自, 中澤 巧爾

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

    　詳細を見る

    開催年月日： 2019年3月

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

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

  30. 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   国名：ニュージーランド  

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

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：ニュージーランド  

  32. 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   国名：グレートブリテン・北アイルランド連合王国(英国)  

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

    Kousuke Fukui and Koji Nakazawa

    7th International Workshop on Confluence (IWC 2018) 

    　詳細を見る

    開催年月日： 2018年7月

    記述言語：英語   会議種別：口頭発表（一般）  

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

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

    仲田 壮佑, 中澤 巧爾

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

    　詳細を見る

    開催年月日： 2018年3月

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

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

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

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    　詳細を見る

    開催年月日： 2017年10月

    記述言語：英語   会議種別：口頭発表（招待・特別）  

    国名：日本国  

  37. 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   国名：ベトナム社会主義共和国  

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

    Koji Nakazawa

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

    　詳細を見る

    開催年月日： 2016年6月

    記述言語：英語   会議種別：口頭発表（一般）  

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

  39. 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   国名：アメリカ合衆国  

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

    K. Nakazawa

    4th International Workshop on Confluence (IWC 2015) 

    　詳細を見る

    開催年月日： 2015年8月

    記述言語：英語   会議種別：口頭発表（招待・特別）  

    国名：日本国  

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

    中澤巧爾, 藤田憲悦

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

    　詳細を見る

    開催年月日： 2015年3月

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

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

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

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

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

    　詳細を見る

    開催年月日： 2015年3月

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

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

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

    K. Nakazawa

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

    　詳細を見る

    開催年月日： 2014年7月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

  44. Extensional model of Lambda-mu calculus

    　詳細を見る

    開催年月日： 2013年9月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

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

    国内共同研究 

▼全件表示

共同研究・競争的資金等の研究課題の先頭へ▲

科研費 18

  1. 論理制約付き項書換えに関する余帰納法に基づくプログラム検証法の開発

    研究課題/研究課題番号：24K02900  2024年4月 - 2029年3月

    科学研究費助成事業  基盤研究(B)

    西田 直樹, 松原 豊, 中澤 巧爾

    　 詳細を見る

    担当区分：研究分担者 

    近年，論理制約付き項書換えシステム（LCTRS）を用いたプログラム検証の研究が盛んになっている．本研究では，検証したいプログラムと性質それぞれをLCTRSとその検証問題に変換および帰着し，帰納法に基づいてその問題を解くプログラム検証法を開発する．帰着する検証問題には等価性問題および全パス到達可能性問題を採用し，その成否の検証を試みる．開発のための具体的な課題として，「等価性問題および全パス到達可能性問題の両方を扱う証明系の形式化と実装」，「等価性・実行時エラー非発生・メモリ安全性など様々な性質からLCTRSの検証問題への帰着」，「検証問題が決定可能となるプログラムと性質の特徴づけ」に取り組む．

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

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

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

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

    　 詳細を見る

    担当区分：研究代表者 

    配分額：4030000円 （ 直接経費：3100000円 、 間接経費：930000円 ）

    循環証明体系は，帰納法に相当する原理を証明の循環構造によって表現する証明体系であり，自動証明との相性が良いことが知られている．本研究では，証明体系の重要な性質である「カット除去可能性」に注目する．カット規則は推論規則の一つであるが，カット規則の適用は自動証明においては不都合である．そのため，カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが，多くの循環証明体系ではカット除去可能性が成立しないことが分かっている．本研究では，論理に制限を課した上でのカット除去可能性や，自動証明の邪魔をしない程度までカット規則を制限できないか，などを明らかにする．
    今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。
    1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。
    2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。
    当初の見込みはおおよそ達成できたが、一階述語論理の循環証明体系に関する予想の証明は想定よりも難航したため解決しなかった。現時点で証明の目処が立ったため、次年度前半までに解決する予定である。
    引き続き、理論的な面では、一階述語論理の言語を制限した循環証明体系におけるカット除去性を調べる。「関数記号なしの場合、循環証明体系はカット除去可能である」ことを予想しているので、これを証明することを目指す。応用面では、とくに分離論理の循環証明体系においてカット論理式にある種の制限を課しても証明能力が変わらないことを示すことにより、自動証明探索に有用な証明体系を模索することを目指す。

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

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

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

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

    　 詳細を見る

    担当区分：研究分担者 

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

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

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

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

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

    　 詳細を見る

    担当区分：研究分担者 

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

  5. 形式言語理論に基づく自動採譜

    研究課題/研究課題番号：23K20392  2020年4月 - 2025年3月

    科学研究費助成事業  基盤研究(B)

    酒井 正彦, 東条 敏, 中澤 巧爾

    　 詳細を見る

    担当区分：研究分担者 

    演奏によって得られたMIDIデータからの品質の高い採譜手法の確立をめざす。演奏は楽譜以上の情報を持つため、演奏のリズムの推定など自動採譜における困難な課題がある。演奏のリズムの推定は、これまでMIDIのノートオン（音のなり始め）イベントの時刻から、（何拍目かという）楽譜上の時刻への対応関係のうち、誤差の少ない関係を出力していた、本研究では、MIDIのイベントの集まりをトークンと呼ぶ塊に分け、その時刻から楽譜上の時刻への対応関係を予測する。これに加えて、リズムを表す重み付き木文法を考慮することで、得られる楽譜の読みやすさをも考慮した自然でリズムが得られることを目指す。
    本研究は、リズムの構造を考慮し自然言語の解析手法の応用により、MIDIデータからの自動採譜手法の確立を目指すことを主な目的としている。
    本年度は主に和音を含む単旋律のリズム量子化について研究を進め、以下の成果が得られた。入力となるmidiイベント列の部分列（トークンと呼ぶ）を、同一時刻に起こる楽譜の単位とみなすことで、MIDI入力と楽譜の要素を対応付ける手法を考案した。具体的にイベントの部分列がトークンとみなせるかどうかを表すいくつかの条件について検討を行い、これをシステムに組み込んで実験を行うことで課題を整理した。このシステムは https://git.trs.css.i.nagoya-u.ac.jp/transcription/qparselib/-/tree/mono2 で公開している。その結果、各イベントが発生した時点で鳴っている音の数を前処理によりあらかじめ計算しておくことによって、処理中に入力のMIDIイベントを参照する範囲が限定でき、その結果効率よくトークンであるかどうかの判定ができることが分かった。また、各イベントを楽譜上の時刻に対応させる際の評価値の計算においてリズムの密度の単旋律における定義の拡張が必要であることが判明した。この評価値は出力の精度に大きく影響があると予想されるため注意が必要である。その他、音楽生成理論に基づく自動演奏に対する表情付アルゴリズムを改良し、それらの実験のためのプラットフォームを作成し公開した。（https://git.trs.css.i.nagoya-u.ac.jp/transcription/dm-env）
    既存のいずれの自動採譜手法においても、MIDIイベントと楽譜の各要素の不一致の解消のために、音の鳴り始めを表すonイベントと音を止めるoffイベントのうちでoffイベントを無視したところから処理を開始していた。この処理により自動採譜におけるさまざまな問題を引き起こしていた。本年度の研究において、この不一致の問題がイベント系列の分かち書きの概念を導入することによって理論的にスッキリと説明でき、分かち書きを含む日本語文の解析に相当する手法を導入することにより解決する手法を考案した。これはブレークスルーとも言え、高精度な自動採譜への道筋が見えてきたといえる。
    これまでに定義した３種類のトークンは、異なる音の高さ（ピッチ）をもつ和音、休符、引き続き音が鳴っていることを表すコンティニュエーションである。ここで和音のトークンは複数の装飾音符を含められるように設計した。そこで、これらのアイデアを自動採譜システムに実装し、実験を行うことにより和音を含む単旋律の自動採譜の精度を高める方向での研究を進める。単旋律のみを扱う場合にも、和音の内まだ鳴り続けているのに一部の音が止まったり、スタッカートの取り扱いなどいくつもの課題が残っている。これらの問題点に対して新たなトークンを導入することで解決できるか、あるいは、他の解決方法を考案する必要があるかなどの検討をおこなう。これらが早期に解決できれば、複旋律が一緒に記録されたMIDI入力に対しても、リズム量子化と旋律分離を同時に行う手法についても検討したい。

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

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

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

    中澤 巧爾, 木村 大輔

    　 詳細を見る

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

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

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

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

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

    　 詳細を見る

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

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

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

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

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

    　 詳細を見る

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

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

    2015年4月 - 2018年3月

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

    中澤巧爾

    　 詳細を見る

    担当区分：研究代表者 

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

    2013年4月 - 2016年3月

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

    五十嵐淳

    　 詳細を見る

    担当区分：研究分担者 

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

    2012年4月 - 2015年3月

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

    中澤巧爾

    　 詳細を見る

    担当区分：研究代表者 

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

    2010年4月 - 2013年3月

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

    佐藤雅彦

    　 詳細を見る

    担当区分：研究分担者 

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

    2009年4月 - 2012年3月

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

    中澤巧爾

    　 詳細を見る

    担当区分：研究代表者 

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

    2007年4月 - 2010年3月

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

    佐藤雅彦

    　 詳細を見る

    担当区分：研究分担者 

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

    2006年4月 - 2009年3月

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

    中澤巧爾

    　 詳細を見る

    担当区分：研究代表者 

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

    2006年4月 - 2007年3月

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

    五十嵐淳

    　 詳細を見る

    担当区分：研究分担者 

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

    2004年4月 - 2006年3月

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

    中澤巧爾

    　 詳細を見る

    担当区分：研究代表者 

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

    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月

    　詳細を見る

    種別：学会・研究会等 

学術貢献活動の先頭へ▲