Updated on 2024/09/18

写真a

 
NAKAZAWA Koji
 
Organization
Graduate School of Informatics Department of Computing and Software Systems 3 Associate professor
Graduate School
Graduate School of Information Science
Graduate School of Informatics
Undergraduate School
School of Engineering Department of Electrical and Electronic Engineering and Information Engineering
School of Informatics Department of Computer Science
Title
Associate professor
Homepage
https://knaknak.github.io/

Degree 1

  1. 博士（理学） （ 2002.11   京都大学 ） 

To the head of Degree.▲

Research History 5

  1. Nagoya University   Graduate School of Informatics Department of Computing and Software Systems 3   Associate professor

    2017.4

  2. Nagoya University   Graduate School of Information Science

    2015.10

  3. Nagoya University   Associate professor

    2015.10 - 2017.3

    　 More details

    Country：Japan

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

    2007.4 - 2015.9

    　 More details

    Country：Japan

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

    2002.12 - 2007.3

    　 More details

    Country：Japan

To the head of Research History.▲

Education 2

  1. Kyoto University   Graduate School, Division of Natural Science

    2000.4 - 2002.11

    　 More details

    Country： Japan

  2. Kyoto University   Faculty of Science

    1994.4 - 1998.3

    　 More details

    Country： Japan

To the head of Education.▲

Professional Memberships 3

  1. European Association for Theoretical Computer Science

  2. 日本数学会

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

To the head of Professional Memberships.▲

Committee Memberships 1

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

    2017.4 - 2021.3   

    　 More details

    Committee type：Academic society

To the head of Committee Memberships.▲

Awards 4

  1. Best Research Paper Award

    2022.9   Spatial Factorization in Cyclic-Proof System for Separation Logic

    Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura

  2. PPL2020論文賞

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

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

    　More details

    Award type：Award from Japanese society, conference, symposium, etc.  Country：Japan

  3. 高橋奨励賞

    2016.9   日本ソフトウェア科学会  

    　More details

    Country：Japan

  4. PPL2006 Best Paper Award

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

    中澤巧爾，龍田真

    　More details

    Award type：Award from Japanese society, conference, symposium, etc.  Country：Japan

To the head of Awards.▲
 

Papers 45

  1. Restriction on cut rule in cyclic-proof system for symbolic heaps Reviewed

    Kenji Saotome, Koji Nakazawa, and Daisuke Kimura

    Theoretical Computer Science   Vol. 1019   2024.12

    　More details

    Authorship：Last author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.tcs.2024.114854

  2. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions Reviewed International journal

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    FSCD 2021, Leibniz International Proceedings in Informatics, LIPIcs   Vol. 195   2021.7

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

    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 Reviewed

    Koji Nakazawa, Ken-etsu Fujita

    Studia Logica     2016.5

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s11225-016-9673-0

  4. Monadic translation of classical sequent calculus Reviewed

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

    Mathematical Structures in Computer Science   Vol. 23 ( 6 ) page： 1111-1162   2013.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1017/S0960129512000436

  5. Type checking and typability in domain-free lambda calculi Reviewed

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

    Theoretical Computer Science   Vol. 412 ( 44 ) page： 6193-6207   2011.10

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.tcs.2011.06.020

  6. Strong normalization of classical natural deduction with disjunctions Reviewed

    K. Nakazawa, M. Tatsuta

    Annals of Pure and Applied Logic   Vol. 153 ( 1-3 ) page： 21-37   2008.4

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.apal.2008.01.003

  7. Strong normalization proof with CPS-translation for second order classical natural deduction Reviewed

    K. Nakazawa, M. Tatsuta

    Journal of Symbolic Logic   Vol. 68 ( 3 ) page： 851-859   2003.9

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.2178/jsl/1067620196

  8. Confluency and strong normalizability of call-by-value lambda-mu calculus Reviewed

    K. Nakazawa

    Theoretical Computer Science   Vol. 290   page： 429-463   2003.1

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

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

  9. Relative completeness of incorrectness separation logic Reviewed

    Yeonseok Lee and Koji nakazawa

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

    　More details

    Authorship：Last author   Language：English   Publishing type：Research paper (international conference proceedings)  

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

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

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

    　More details

    Authorship：Last author   Language：Japanese   Publishing type：Research paper (conference, symposium, etc.)  

  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

    Computer Software   Vol. 41 ( 1 ) page： 1_50 - 1_67   2024.1

    　More details

    Language：Japanese   Publisher：Japan Society for Software Science and Technology  

    <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

    Other Link： https://ndlsearch.ndl.go.jp/books/R000000004-I033331532

  12. Decidable entailment checking for concurrent separation logic with fractional permissions

    LEE Yeonseok, NAKAZAWA Koji

    Computer Software   Vol. 40 ( 4 ) page： 4_67 - 4_86   2023.10

    　More details

    Language：Japanese   Publisher：Japan Society for Software Science and Technology  

    <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

    Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

    Mathematical Structures in Computer Science   Vol. 32 ( 7 ) page： 1015 - 1027   2022.8

    　More details

    Publishing type：Research paper (scientific journal)   Publisher：Cambridge University Press (CUP)  

    ABSTRACT

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

    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   Vol. 2228   page： 59 - 72   2022.8

    　More details

    Language：English  

    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性について (証明と計算の理論と応用)

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

    数理解析研究所講究録   Vol. 2228   page： 30 - 40   2022.8

    　More details

    Language：Japanese   Publisher：京都大学数理解析研究所  

    CiNii Research

  16. Biabduction for separation logic with arrays and lists Reviewed

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

        2022.3

    　More details

    Language：English   Publishing type：Research paper (conference, symposium, etc.)  

  17. Confluence Proofs of Lambda-Mu-Calculi by Z Theorem Reviewed

    Yuki Honda, Koji Nakazawa, and Ken-etsu Fujita

    Studia Logica   Vol. 109 ( 5 ) page： 917 - 936   2021.10

    　More details

    Language：Japanese   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s11225-020-09931-0

    Web of Science

    Scopus

  18. Function Pointer Eliminator for C Programs Reviewed International coauthorship International journal

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

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   Vol. 13008   page： 23 - 37   2021

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer Science and Business Media Deutschland GmbH  

    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 Reviewed

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    The 15th International Symposium on Functional and Logic Programming (FLOPS 2020)     page： .   2020.9

    　More details

    Language：English  

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

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

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

    　More details

    Language：Japanese  

  21. Failure of Cut-Elimination in Cyclic Proofs of Separation Logic Reviewed

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

      Vol. 37 ( 1 ) page： 39-52   2020.2

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

  22. Spatial Factorization in Cyclic-Proof System for Separation Logic Reviewed

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

        page： .   2020

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

  23. Failure of Cut-Elimination in Cyclic Proofs of Separation Logic Reviewed

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

        page： .   2019.3

    　More details

    Language：English  

  24. Spatial Factorization in Cyclic-Proof System for Separation Logic Reviewed

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

        page： .   2019.3

    　More details

    Authorship：Lead author   Language：English  

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

    井上 鉄也, 中澤 巧爾

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

    　More details

    Language：Japanese  

  26. Z for call-by-value Reviewed

    Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

    6th International Workshop on Cofluence (IWC 2017),     page： 57–61   2017.9

    　More details

    Authorship：Lead author   Language：English  

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

    仲田 壮佑, 中澤 巧爾

    日本ソフトウェア科学会第33回大会講演論文集     page： .   2016.9

    　More details

    Language：Japanese  

    DOI： .

  28. Church-Rosser theorem and compositional Z-property

    Ken-etsu Fujita, Koji Nakazawa

        page： .   2016.9

    　More details

    Language：English  

    DOI： .

  29. Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild Reviewed

    Takeshi Tsukada, Koji Nakazawa

        page： .   2016.3

    　More details

    Language：English  

    DOI： .

  30. Compositional Z: Confluence proofs for permutative conversion

    K. Nakazawa, K. Fujita

        page： .   2015.9

    　More details

    Authorship：Lead author   Language：English  

    DOI： .

  31. Strong reduction of combinatory logic with streams Reviewed

    K. Nakazawa, H. Naya

    Studia Logica   Vol. 103   page： 375-387   2015.4

    　More details

    Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s11225-014-9570-3

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

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

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

    　More details

    Language：Japanese  

    DOI： .

  33. Reduction system for extensional lambda-mu calculus Reviewed

    Koji Nakazawa and Tomoharu Nagai

    Lecture Notes in Computer Science (RTA-TLCA 2014)   Vol. 8560   page： 340-363   2014.7

    　More details

    Authorship：Lead author   Language：English  

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

  34. Confluence for classical logic through the distinction between values and computation Reviewed

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

    Electric Proceedings in Theoretical Computer Science (CL&C 2014)   Vol. 164   page： 63-77   2014.7

    　More details

    Language：English  

    DOI： 10.4204/EPTCS.164.5

  35. Extensional models of untyped lambda-mu calculus Reviewed

    Koji Nakazawa and Shin-ya Katsumata

    Electric Proceedings in Theoretical Computer Science (CL&C 2012)   Vol. 97   page： 35-47   2012.10

    　More details

    Authorship：Lead author   Language：English  

    DOI： 10.4204/EPTCS.97.3

  36. Combinators for streams

    K. Nakazawa

        page： CD-ROM   2011.9

    　More details

    Authorship：Lead author   Language：English  

    DOI： CD-ROM

  37. Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems Reviewed

        page： Article 7   2010

    　More details

    Authorship：Lead author   Language：Japanese   Publishing type：Research paper (scientific journal)  

  38. Type checking and inference are equivalent in lambda calculi with existential types Reviewed

    Y. Kato, K. Nakazawa

    Lecture Notes in Computer Science (WFLP 2009)   Vol. 5979   page： 96-110   2010

    　More details

    Language：English  

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

  39. Type checking and inference for polymorphic and existential types Reviewed

    K. Nakazawa, M. Tatsuta

    Conferences in Research and Practice in Information Technology Series   Vol. 94   page： .   2009

    　More details

    Authorship：Lead author   Language：English  

  40. Undecidability of type-checking in domain-free typed lambda-calculi with existence Reviewed

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

    Lecture Notes in Computer Science (CSL 2008)   Vol. 5213   page： 478-492   2008.9

    　More details

    Authorship：Lead author   Language：English  

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

  41. An isomorphism between cut-elimination procedure and proof reduction Reviewed

    K. Nakazawa

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   Vol. 4583 LNCS   page： 336-350   2007

    　More details

    Language：English  

  42. Strong normalization proofs by CPS-translations Reviewed

    S. Ikeda, K. Nakazawa

    Information Processing Letters   Vol. 99 ( 4 ) page： 163-170   2006.8

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.ipl.2006.03.009

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

    中澤 巧爾, 龍田 真

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

    　More details

    Language：Japanese  

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

    池田 聡, 中澤 巧爾

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

    　More details

    Language：Japanese  

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

    中澤巧爾

    日本ソフトウェア科学会第17回大会講演論文集     page： CD-ROM   2000.9

    　More details

    Authorship：Lead author   Language：Japanese  

    DOI： CD-ROM

▼display all

To the head of Papers.▲

Books 2

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

    Winskel Glynn, 勝股 審也, 中澤 巧爾, 西村 進 , 前田 敦司 , 末永 幸平（ Role： Joint translator ,  10〜11章）

    丸善出版  2023  （ ISBN:9784621307632 ）

    　More details

    Responsible for pages：183-242   Language：Japanese Book type：Scholarly book

    CiNii Books

  2. 理論計算機科学事典

    徳山 豪，小林 直樹(総編集)（ Role： Contributor ,  8.2章）

    2022.1 

    　More details

    Total pages：816   Language：Japanese Book type：Dictionary, encyclopedia

To the head of Books.▲

Presentations 45

  1. Relative completeness of incorrectness separation logic

    Koji Nakazawa and Yeonseok Lee

    2024.8 

    　More details

    Event date： 2024.8

    Language：Japanese   Presentation type：Oral presentation (general)  

    Country：Japan  

  2. Toward completeness of incorrectness separation logic

    Lee Yeonseok and Koji Nakazawa

    2024.3 

    　More details

    Event date： 2024.3

    Language：English   Presentation type：Poster presentation  

    Country：Japan  

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

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

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

    　More details

    Event date： 2024.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：新潟   Country：Japan  

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

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

    RIMS共同研究「証明論と計算論の最前線」  2023.12.11 

    　More details

    Event date： 2023.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：京都大学   Country：Japan  

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

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

    日本数学会秋季総合分科会  2022.9  日本数学会

    　More details

    Event date： 2022.9

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：北海道大学   Country：Japan  

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

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

    SLACS 2022  2022.9 

    　More details

    Event date： 2022.9

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：東邦大学   Country：Japan  

  7. Decidable entailment checking for concurrent separation logic with fractional permissions International coauthorship

    Yeonseok Lee, Koji Nakazawa

    2022.8.31 

    　More details

    Event date： 2022.8 - 2022.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

  8. Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions International coauthorship

    2022.3.6 

    　More details

    Event date： 2022.3

    Language：English   Presentation type：Poster presentation  

    Country：Japan  

  9. 無限証明体系と循環証明体系の証明能力同等性 International coauthorship

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

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

    　More details

    Event date： 2022.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：オンライン   Country：Japan  

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

    石井沙織，中澤巧爾

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

    　More details

    Event date： 2022.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：オンライン   Country：Japan  

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

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

    RIMS共同研究「証明と計算の理論と応用」  2021.12.20 

    　More details

    Event date： 2021.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：京都大学   Country：Japan  

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

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

    RIMS共同研究「証明と計算の理論と応用」  2021.12.20 

    　More details

    Event date： 2021.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：京都大学   Country：Japan  

  13. 分離論理 Invited

    中澤 巧爾

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

    　More details

    Event date： 2021.9

    Language：Japanese   Presentation type：Public lecture, seminar, tutorial, course, or other speech  

    Venue：オンライン   Country：Japan  

  14. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions International conference

    Koji Nakazawa, Kenji Saotome, Daisuke Kimura

    Forth Workshop on Mathematical Logic and its Applications (MLA 2021)  2021.3 

    　More details

    Event date： 2021.3

    Language：English   Presentation type：Oral presentation (general)  

    Venue：online   Country：Japan  

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

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

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

    　More details

    Event date： 2021.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：オンライン   Country：Japan  

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

    早乙女 献自, 中澤 巧爾

    SLACS 2020  2020.12 

    　More details

    Event date： 2020.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：オンライン   Country：Japan  

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

    本多 雄樹, 中澤 巧爾

    SLACS 2020  2020.12 

    　More details

    Event date： 2020.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：オンライン   Country：Japan  

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

    本多 雄樹，中澤 巧爾

    日本ソフトウェア科学会第 37 回大会  2020.9  日本ソフトウェア科学会

    　More details

    Event date： 2020.9

    Language：Japanese   Presentation type：Oral presentation (general)  

    Venue：オンライン   Country：Japan  

  19. Proof Normalization for Classical Truth-Table Natural Deduction

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

    2020.9 

    　More details

    Event date： 2020.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

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

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

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

    　More details

    Event date： 2020.2

    Language：Japanese   Presentation type：Poster presentation  

    Venue：オンライン   Country：Japan  

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

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

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

    　More details

    Event date： 2020.2

    Language：Japanese   Presentation type：Poster presentation  

    Venue：オンライン   Country：Japan  

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

    　More details

    Event date： 2019.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Country：Japan  

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

    　More details

    Event date： 2019.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Country：Japan  

  24. Proof normalization for classical truth-table natural deduction

    　More details

    Event date： 2019.12

    Language：Japanese   Presentation type：Oral presentation (general)  

    Country：Japan  

  25. On cut elimination in cyclic-proof systems International conference

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

    The 51st TRS Meeting 

    　More details

    Event date： 2019.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

  26. Confluence Proof of lambda-mu-Calculus by Z Theorem International conference

    Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita

    The 51st TRS Meeting 

    　More details

    Event date： 2019.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

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

    中澤 巧爾

    日本数学会2019年度年会 

    　More details

    Event date： 2019.3

    Language：Japanese   Presentation type：Oral presentation (invited, special)  

    Country：Japan  

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

    本多 雄樹, 中澤 巧爾

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

    　More details

    Event date： 2019.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：花巻市   Country：Japan  

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

    早乙女 献自, 中澤 巧爾

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

    　More details

    Event date： 2019.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：花巻市   Country：Japan  

  30. On Cut-Elimination in Cyclic Proof Systems International conference

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

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

    　More details

    Event date： 2018.12

    Language：English   Presentation type：Poster presentation  

    Venue：Wellington   Country：New Zealand  

  31. On Cut-Elimination in Cyclic Proof Systems International conference

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

    Workshop on New Ideas and Emerging Results (NIER 2019) 

    　More details

    Event date： 2018.12

    Language：English   Presentation type：Oral presentation (general)  

    Country：New Zealand  

  32. Cyclic Theorem Prover for Separation Logic by Magic Wand. International conference

    Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura

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

    　More details

    Event date： 2018.7

    Language：English   Presentation type：Oral presentation (general)  

    Venue：Oxford, UK   Country：United Kingdom  

  33. Complete Axiom System of Cluster Algebra International conference

    Kousuke Fukui and Koji Nakazawa

    7th International Workshop on Confluence (IWC 2018) 

    　More details

    Event date： 2018.7

    Language：English   Presentation type：Oral presentation (general)  

    Venue：Oxford, UK   Country：United Kingdom  

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

    仲田 壮佑, 中澤 巧爾

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

    　More details

    Event date： 2018.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：米子市   Country：Japan  

  35. Completeness of Cyclic Proofs for Symbolic Heaps. International conference

    Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura

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

    　More details

    Event date： 2018.3

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

  36. Complete cyclic-proof system for separation logic with general inductive predicates Invited International conference

    　More details

    Event date： 2017.10

    Language：English   Presentation type：Oral presentation (invited, special)  

    Country：Japan  

  37. Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions International conference

    Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa

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

    　More details

    Event date： 2016.11

    Language：English   Presentation type：Oral presentation (general)  

    Venue：Halong Bay, Vietnam   Country：Viet Nam  

  38. Characterizing trees for lambda-mu terms International conference

    Koji Nakazawa

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

    　More details

    Event date： 2016.6

    Language：English   Presentation type：Oral presentation (general)  

    Venue：Porto, Portugal   Country：Portugal  

  39. A denotational semantics of a probabilistic stream-processing language International conference

    Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa

    Workshop on probabilistic programming semantics (PPS 2016) 

    　More details

    Event date： 2016.1

    Language：English   Presentation type：Poster presentation  

    Venue：Florida, US   Country：United States  

  40. Lambda calculi and confluence from A to Z International conference

    K. Nakazawa

    4th International Workshop on Confluence (IWC 2015) 

    　More details

    Event date： 2015.8

    Language：English   Presentation type：Oral presentation (invited, special)  

    Country：Japan  

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

    中澤巧爾, 藤田憲悦

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

    　More details

    Event date： 2015.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：松山   Country：Japan  

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

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

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

    　More details

    Event date： 2015.3

    Language：Japanese   Presentation type：Poster presentation  

    Venue：松山   Country：Japan  

  43. Extensional models of typed lambda-mu calculus International conference

    K. Nakazawa

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

    　More details

    Event date： 2014.7

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

  44. Extensional model of Lambda-mu calculus

    　More details

    Event date： 2013.9

    Language：Japanese   Presentation type：Oral presentation (general)  

    Country：Japan  

  45. Continuations and classical logic: using continuations as a tool for classical logic International conference

    K. Nakazawa

    Continuation Workshop (CW2011) 

    　More details

    Event date： 2011.9

    Language：English   Presentation type：Oral presentation (invited, special)  

    Country：Japan  

▼display all

To the head of Presentations.▲

Research Project for Joint Research, Competitive Funding, etc. 10

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

    Grant number：21FP01  2021.4 - 2022.3

    公募型共同研究 

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

    　 More details

    Authorship：Principal investigator  Grant type：Competitive

    Grant amount：\190000

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

    Grant number：20FP03  2020.4 - 2021.3

    公募型共同研究 

    中澤 巧爾，龍田 真

    　 More details

    Authorship：Principal investigator  Grant type：Competitive

    Grant amount：\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

    国内共同研究 

▼display all

To the head of Research Project for Joint Research, Competitive Funding, etc..▲

KAKENHI (Grants-in-Aid for Scientific Research) 18

  1. Development of Program Verification Techniques Based on Coinduction on Logically Constrained Rewriting

    Grant number：24K02900  2024.4 - 2029.3

    Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (B)

    　 More details

    Authorship：Coinvestigator(s) 

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

    Grant number：22K11901  2022.4 - 2026.3

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

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

    　 More details

    Authorship：Principal investigator 

    Grant amount：\4030000 （ Direct Cost: \3100000 、 Indirect Cost：\930000 ）

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

  3. Network of automata with data based on compositional active learning

    Grant number：21H03415  2021.4 - 2026.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)  Grant-in-Aid for Scientific Research (B)

    　 More details

    Authorship：Coinvestigator(s) 

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

    Grant number：21H03421  2021.4 - 2024.3

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

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

    　 More details

    Authorship：Coinvestigator(s) 

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

  5. Automated transcription based on formal language theory

    Grant number：23K20392  2020.4 - 2025.3

    Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (B)

    　 More details

    Authorship：Coinvestigator(s) 

  6. Proof theoretic analysis of cyclic proof systems

    Grant number：18K11161  2018.4 - 2021.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)  Grant-in-Aid for Scientific Research (C)

    Nakazawa Koji

    　 More details

    We investigate proof theoretic properties of cyclic proof systems, and we obtain the following results. (1) We show that the cut-elimination fails in the cyclic proof system for the symbolic heap separation logic. (2) We show that the restriction of the cut rule to extended subformulas of the bottom sequent in that system properly changes the provability. (3) We show that the cut-elimination fails in the cyclic proof system for the bunched logic.

  7. A reversible debugging model for real-time concurrent programs

    Grant number：17H01722  2017.4 - 2021.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)  Grant-in-Aid for Scientific Research (B)

    YUEN SHOJI

    　 More details

    The objectives of this research seek a technology based on reversible computing to provide a novel technique for analysing concurrent programs. Recent software technology of development and maintenance requires behavioural analysis with the past configurations. Concurrency often makes such analysis difficult since the behaviour is inherently nondeterministic, and a replay of execution involves the information of forward executions, which are usually discarded.
    In this respect, we investigate a technique base on the formal model analysing reversible execution of concurrent software. We apply the technique to the behaviour analysis, mainly aiming at efficient debugging of concurrent programs. We also investigate analysis techniques for concurrent programs and debuggers, including information compression, timed automaton model, and session types.

  8. Theory of Gradual Typing for Modern Programming Languages

    Grant number：17H01723  2017.4 - 2021.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)  Grant-in-Aid for Scientific Research (B)

    Atsushi Igarashi

    　 More details

    Gradual typing is a programming-language technique that allows statically typed and dynamically typed parts to coexist in a single program. We have studied the theoretical foundations for applying this technique to advanced programming languages. The main result is computational calculi that introduce gradual typing to advanced programming language mechanisms such as polymorphism, session types, refinement types, nondeterminism, ML type inference, and intersection types; we have proved its properties (such as type safety). In addition, we improved space-efficient coercions that have been proposed as an implementation technique for gradual typing by coercion passing style compilation, which we implemented and evaluated.

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

    2015.4 - 2018.3

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

    中澤巧爾

    　 More details

    Authorship：Principal investigator 

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

    2013.4 - 2016.3

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

    五十嵐淳

    　 More details

    Authorship：Coinvestigator(s) 

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

    2012.4 - 2015.3

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

    中澤巧爾

    　 More details

    Authorship：Principal investigator 

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

    2010.4 - 2013.3

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

    佐藤雅彦

    　 More details

    Authorship：Coinvestigator(s) 

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

    2009.4 - 2012.3

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

    中澤巧爾

    　 More details

    Authorship：Principal investigator 

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

    2007.4 - 2010.3

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

    佐藤雅彦

    　 More details

    Authorship：Coinvestigator(s) 

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

    2006.4 - 2009.3

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

    中澤巧爾

    　 More details

    Authorship：Principal investigator 

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

    2006.4 - 2007.3

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

    五十嵐淳

    　 More details

    Authorship：Coinvestigator(s) 

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

    2004.4 - 2006.3

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

    中澤巧爾

    　 More details

    Authorship：Principal investigator 

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

    2004.4 - 2006.3

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

    佐藤雅彦

    　 More details

    Authorship：Coinvestigator(s) 

▼display all

To the head of KAKENHI (Grants-in-Aid for Scientific Research).▲
 

Teaching Experience (On-campus) 3

  1. 基礎セミナー

    2016

    　詳細を見る

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

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

    2016

    　詳細を見る

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

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

    2015

    　詳細を見る

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

To the head of Teaching Experience (On-campus).▲

Teaching Experience (Off-campus) 2

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

    （Nagoya University）

  2. 基礎セミナー

    （Nagoya University）

To the head of Teaching Experience (Off-campus).▲
 

Academic Activities 2

  1. FLOPS 2020 program committee member International contribution

    Role(s)：Peer review

    2020.9

    　More details

    Type：Academic society, research group, etc. 

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

    Role(s)：Planning, management, etc.

    日本ソフトウェア科学会プログラミング論研究会  2017.4 - 2021.3

    　More details

    Type：Academic society, research group, etc. 

To the head of Academic Activities.▲