Updated on 2024/02/22
博士（理学） （ 2002.11 京都大学 ）
Nagoya University Graduate School of Informatics Department of Computing and Software Systems 3 Associate professor
2017.4
Nagoya University Associate professor
2015.10 - 2017.3
Country：Japan
京都大学大学院情報学研究科助教
2007.4 - 2015.9
Country：Japan
京都大学大学院情報学研究科助手
2002.12 - 2007.3
Country：Japan
Kyoto University Graduate School, Division of Natural Science
2000.4 - 2002.11
Country： Japan
Kyoto University Faculty of Science
1994.4 - 1998.3
Country： Japan
European Association for Theoretical Computer Science
日本数学会
日本ソフトウェア科学会
日本ソフトウェア科学会プログラミング論研究会運営委員 運営委員
2017.4 - 2021.3
Committee type：Academic society
Best Research Paper Award
2022.9 Spatial Factorization in Cyclic-Proof System for Separation Logic
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura
PPL2020論文賞
2020.3 日本ソフトウェア科学会プログラミング論研究会 古典論理に対する汎用的自然演繹の証明正規化
福井 康介, 中澤 巧爾, 石井 沙織, 結縁 祥治
高橋奨励賞
2016.9 日本ソフトウェア科学会
PPL2006 Best Paper Award
2006.3 日本ソフトウェア科学会プログラミング論研究会 選言を含む自然演繹古典論理の強正規化性
中澤巧爾，龍田真
Bi-abduction in separation logic with arrays and lists for program analysis Reviewed International coauthorship
Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Mirai Ikebuchi, Koji Nakazawa
Computer Software Vol. 41 ( 1 ) page： 50 - 67 2024.1
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
Cut-elimination for cyclic proof systems with inductively defined propositions
Daisuke Kimura, Koji Nakazawa, Kenji Saotome
RIMS Kokyuroku Vol. 2228 page： 59 - 72 2022.8
合流性とZ定理について
赤坂 陸来, 藤田 憲悦, 中澤 巧爾
数理解析研究所講究録 Vol. 2228 page： 30 - 40 2022.8
Z property for the shuffling calculus
Nakazawa Koji, Fujita Ken-etsu, Imagawa Yuta
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE Vol. 32 ( 7 ) page： 1015 - 1027 2022.8
合流性とZ性について (証明と計算の理論と応用)
赤坂 陸来, 藤田 憲悦, 中澤 巧爾
数理解析研究所講究録 Vol. 2228 page： 30 - 40 2022.8
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
Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions Reviewed International journal
Saotome K., Nakazawa K., Kimura D.
Leibniz International Proceedings in Informatics, LIPIcs Vol. 195 2021.7
Function Pointer Eliminator for C Programs Reviewed International coauthorship International journal
Kimura D., Al Ameen M.F., Tatsuta M., Nakazawa K.
Lecture Note in Computer Science Vol. 13008 page： 23 - 37 2021
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
古典論理に対する汎用的自然演繹の証明正規化 Reviewed
福井 康介, 中澤 巧爾, 石井 沙織, 結縁 祥治
第22回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2020) page： . 2020.3
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
Spatial Factorization in Cyclic-Proof System for Separation Logic Reviewed
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura
page： . 2020
Failure of Cut-Elimination in Cyclic Proofs of Separation Logic Reviewed
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
page： . 2019.3
Spatial Factorization in Cyclic-Proof System for Separation Logic Reviewed
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura
page： . 2019.3
高階契約に対するトレース意味論の完全抽象性 Reviewed
井上 鉄也, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)論文集 page： . 2018.3
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
帰納的述語定義を含む分離論理における循環証明による半自動証明
仲田 壮佑, 中澤 巧爾
日本ソフトウェア科学会第33回大会講演論文集 page： . 2016.9
Church-Rosser theorem and compositional Z-property
Ken-etsu Fujita, Koji Nakazawa
page： . 2016.9
Compositional Z: Confluence proofs for permutative conversion Reviewed
Koji Nakazawa, Ken-etsu Fujita
Studia Logica 2016.5
Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild Reviewed
Takeshi Tsukada, Koji Nakazawa
page： . 2016.3
Compositional Z: Confluence proofs for permutative conversion
K. Nakazawa, K. Fujita
page： . 2015.9
Strong reduction of combinatory logic with streams Reviewed
K. Nakazawa, H. Naya
Studia Logica Vol. 103 page： 375-387 2015.4
高階契約を持つプログラミング言語に対するトレース意味論 Reviewed
村井 涼, 五十嵐 淳, 中澤 巧爾
第17回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2015) page： . 2015.3
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
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
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
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
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
Combinators for streams
K. Nakazawa
page： CD-ROM 2011.9
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems Reviewed
page： Article 7 2010
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
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
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
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
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
Strong normalization proofs by CPS-translations Reviewed
S. Ikeda, K. Nakazawa
Information Processing Letters Vol. 99 ( 4 ) page： 163-170 2006.8
選言を含む自然演繹古典論理の強正規化性 Reviewed
中澤 巧爾, 龍田 真
第8回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2006), page： . 2006
コントロールオペレータをもつ計算体系の強正規化可能性のCPS変換を用いた証明 Reviewed
池田 聡, 中澤 巧爾
第7回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2005), 171--186 page： . 2005
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
Confluency and strong normalizability of call-by-value lambda-mu calculus Reviewed
K. Nakazawa
Theoretical Computer Science Vol. 290 page： 429-463 2003.1
値呼びラムダ・ミュー計算の合流性と強正規化性
中澤巧爾
日本ソフトウェア科学会第17回大会講演論文集 page： CD-ROM 2000.9
Winskel Glynn, 勝股 審也, 中澤 巧爾, 西村 進, 前田 敦司, 末永 幸平（ Role： Joint translator , 10〜11章）
丸善出版 2023 （ ISBN:9784621307632 ）
徳山 豪，小林 直樹(総編集)（ Role： Contributor , 8.2章）
2022.1
Z定理のモジュール性
女屋優貴，藤田憲悦，中澤巧爾
RIMS共同研究「証明論と計算論の最前線」 2023.12.11
命題論理に対する無限証明体系と循環証明体系の証明能力同等性
堀弘昌, 中澤巧爾, 龍田真
日本数学会秋季総合分科会 2022.9 日本数学会
不動点演算子を持つ命題論理の循環証明体系
中澤巧爾, 堀弘昌, 龍田真
SLACS 2022 2022.9
Decidable entailment checking for concurrent separation logic with fractional permissions International coauthorship
Yeonseok Lee, Koji Nakazawa
2022.8.31
Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions International coauthorship
2022.3.6
無限証明体系と循環証明体系の証明能力同等性 International coauthorship
堀弘昌，中澤巧爾，龍田真
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022.3.7 日本ソフトウェア科学会プログラミング論研究会
制限された帰納的述語を含む分離論理の完全な循環証明体系 International coauthorship
石井沙織，中澤巧爾
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022.3.7 日本ソフトウェア科学会プログラミング論研究会
帰納的命題を含む循環証明体系のカット除去
中澤巧爾，早乙女献自，木村大輔
RIMS共同研究「証明と計算の理論と応用」 2021.12.20
合流性とZ定理について
赤坂陸来，藤田憲悦，中澤巧爾
RIMS共同研究「証明と計算の理論と応用」 2021.12.20
分離論理 Invited
中澤 巧爾
2021年度数学基礎論サマースクール（古典論理に限らない論理） 2021.9 日本数学会
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
分離論理におけるエンテイルメント判定問題の決定不能性
飯田 晟樹，早乙女 献自，中澤 巧爾
第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021) 日本ソフトウェア科学会プログラミング論研究会
分離論理の循環証明体系における帰納的述語の制限とカット除去
早乙女 献自, 中澤 巧爾
SLACS 2020 2020.12
書換え系の変換を用いたZ性の証明
本多 雄樹, 中澤 巧爾
SLACS 2020 2020.12
書換え系の変換を用いたZ性の証明
本多 雄樹，中澤 巧爾
日本ソフトウェア科学会第 37 回大会 2020.9 日本ソフトウェア科学会
Proof Normalization for Classical Truth-Table Natural Deduction
Kosuke Fukui, Saori Ishii, Koji Nakazawa, and Takeshi Tsukada
2020.9
分離論理におけるエンテイルメント証明器の入力に対する制限の緩和
青木 洸佑, 中澤 巧爾, 木村 大輔
第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) 日本ソフトウェア科学会プログラミング論研究会
分離論理における記号ヒープのための循環証明体系におけるカットの制限について
早乙女 献自, 中澤 巧爾, 木村 大輔
第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) 日本ソフトウェア科学会プログラミング論研究会
On restricted cut-elimination for cyclic proof system for separation logic
Confluence proof of lambda-mu-calculus by Z thorem
Proof normalization for classical truth-table natural deduction
On cut elimination in cyclic-proof systems International conference
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
The 51st TRS Meeting
Confluence Proof of lambda-mu-Calculus by Z Theorem International conference
Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita
The 51st TRS Meeting
プログラムの正しさを証明する ---分離論理入門--- Invited
中澤 巧爾
日本数学会2019年度年会
Z定理を用いたラムダ・ミュー計算の合流性証明
本多 雄樹, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
循環証明体系における準カット除去可能性について
早乙女 献自, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
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)
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)
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)
Complete Axiom System of Cluster Algebra International conference
Kousuke Fukui and Koji Nakazawa
7th International Workshop on Confluence (IWC 2018)
帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出
仲田 壮佑, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
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)
Complete cyclic-proof system for separation logic with general inductive predicates Invited International conference
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
Characterizing trees for lambda-mu terms International conference
Koji Nakazawa
8th International Workshop on Higher-Order Rewriting (HOR 2016)
A denotational semantics of a probabilistic stream-processing language International conference
Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa
Workshop on probabilistic programming semantics (PPS 2016)
Lambda calculi and confluence from A to Z International conference
K. Nakazawa
4th International Workshop on Confluence (IWC 2015)
置換簡約を含むラムダ計算の合流性
中澤巧爾, 藤田憲悦
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
京都大学 teen racketeer 養成コース
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
Extensional models of typed lambda-mu calculus International conference
K. Nakazawa
The Fifth International Workshop on Classical Logic and Computation (CL&C'14)
Extensional model of Lambda-mu calculus
Continuations and classical logic: using continuations as a tool for classical logic International conference
K. Nakazawa
Continuation Workshop (CW2011)
分離論理における帰納的述語とエンテイルメント判定問題
Grant number：21FP01 2021.4 - 2022.3
公募型共同研究
中澤 巧爾，龍田 真，木村 大輔，Mahmudul Faisal Al Ameen
Authorship：Principal investigator Grant type：Competitive
Grant amount：\190000
制限された帰納的述語をもつ循環証明体系のカット除去可能性
Grant number：20FP03 2020.4 - 2021.3
公募型共同研究
中澤 巧爾，龍田 真
Authorship：Principal investigator Grant type：Competitive
Grant amount：\376000
ストリーム計算のための型システム
2013.4 - 2014.3
国内共同研究
ストリームを扱う計算体系とそのモデル
2012.4 - 2013.3
国内共同研究
暗黙的に型付けされた多相型・存在型を含むラムダ計算
2011.4 - 2012.3
国内共同研究
型推論が決定可能な存在型を含む型付ラムダ計算
2010.4 - 2011.3
国内共同研究
多相型・存在型を含む型付きラムダ計算における型検査問題
2009.4 - 2010.3
国内共同研究
簡単共通部分型理論とラムダ計算のモデルについて
2008.4 - 2009.3
国内共同研究
古典シーケント計算の計算論的意味
2007.4 - 2008.3
国内共同研究
古典論理に対応する型理論
2006.4 - 2007.3
国内共同研究
Grant number：22K11901 2022.4 - 2026.3
日本学術振興会 科学研究費助成事業 基盤研究(C) 基盤研究(C)
中澤 巧爾, 木村 大輔, 木村 大輔
Authorship：Principal investigator
Grant amount：\4030000 （ Direct Cost: \3100000 、 Indirect Cost：\930000 ）
循環証明体系は，帰納法に相当する原理を証明の循環構造によって表現する証明体系であり，自動証明との相性が良いことが知られている．本研究では，証明体系の重要な性質である「カット除去可能性」に注目する．カット規則は推論規則の一つであるが，カット規則の適用は自動証明においては不都合である．そのため，カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが，多くの循環証明体系ではカット除去可能性が成立しないことが分かっている．本研究では，論理に制限を課した上でのカット除去可能性や，自動証明の邪魔をしない程度までカット規則を制限できないか，などを明らかにする．
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)
Authorship：Coinvestigator(s)
Grant number：21H03421 2021.4 - 2024.3
日本学術振興会 科学研究費助成事業 基盤研究(B) 基盤研究(B)
龍田 真, 中澤 巧爾, 木村 大輔, 中澤 巧爾, 木村 大輔
Authorship：Coinvestigator(s)
ソフトウェア検証理論として近年よい理論(オハーン理論)が提案され理論的にも実用的にも成功しているが, 精度がまだ不十分である. 本研究の大目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することである. 本研究の目的は, オハーン理論に一般的述語, 配列, 算術を追加した論理体系に対して, 関数の再帰呼出しを追加し, 再帰データを追加し, また, 関数ポインタ呼出しを追加し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. この実装システムを用いてOpenSSLおよびgitのCコードのメモリー安全性を検証する.
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
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.
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
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.
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
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.
計算における無限概念と古典論理
2015.4 - 2018.3
科学研究費補助金 基盤研究(C)
中澤巧爾
Authorship：Principal investigator
ソフトウェア契約に基づく高階型付プログラムの理論
2013.4 - 2016.3
科学研究費補助金 基盤研究(A)
五十嵐淳
Authorship：Coinvestigator(s)
ストリーム計算のための計算モデル
2012.4 - 2015.3
科学研究費補助金 若手研究(B)
中澤巧爾
Authorship：Principal investigator
バグのないソフトウェア構築環境に関する研究の新展開
2010.4 - 2013.3
科学研究費補助金 基盤研究(B)
佐藤雅彦
Authorship：Coinvestigator(s)
二階存在量化子をもつ計算体系
2009.4 - 2012.3
科学研究費補助金 若手研究(B)
中澤巧爾
Authorship：Principal investigator
計算と論理の融合によるバグのないソフトウェア構築環境に関する研究
2007.4 - 2010.3
科学研究費補助金 基盤研究(B)
佐藤雅彦
Authorship：Coinvestigator(s)
古典論理の構文論的双対性とその計算論的意味
2006.4 - 2009.3
科学研究費補助金 若手研究(B)
中澤巧爾
Authorship：Principal investigator
安全・安心な環境適応型ソフトウェアの基礎理論に関する研究
2006.4 - 2007.3
科学研究費補助金 特定領域研究
五十嵐淳
Authorship：Coinvestigator(s)
古典論理に基づく非決定的計算体系
2004.4 - 2006.3
科学研究費補助金 若手研究(B)
中澤巧爾
Authorship：Principal investigator
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
2004.4 - 2006.3
科学研究費補助金 特定領域研究
佐藤雅彦
Authorship：Coinvestigator(s)
基礎セミナー
2016
プログラミング基礎及び演習
2016
プログラミング基礎及び演習
2015
プログラミング基礎及び演習
（Nagoya University）
基礎セミナー
（Nagoya University）
FLOPS 2020 program committee member International contribution
Role(s)：Peer review
2020.9
日本ソフトウェア科学会プログラミング論研究会運営委員
Role(s)：Planning, management, etc.
日本ソフトウェア科学会プログラミング論研究会 2017.4 - 2021.3
