中澤巧爾 Nakazawa Koji

研究者番号	80362581
その他のID
所属 (現在)	2025年度: 名古屋大学, 情報学研究科, 准教授
所属 (過去の研究課題情報に基づく) *注記	2017年度 – 2024年度: 名古屋大学, 情報学研究科, 准教授 2015年度 – 2016年度: 名古屋大学, 情報科学研究科, 准教授 2007年度 – 2014年度: 京都大学, 情報学研究科, 助教 2011年度 – 2012年度: 京都大学, 大学院・情報学研究科, 助教 2008年度 – 2009年度: 京都大学, 大学院・情報学研究科, 助教 2003年度 – 2006年度: 京都大学, 情報学研究科, 助手
審査区分/研究分野	研究代表者情報学基礎 / 小区分60010:情報学基礎論関連 / 情報学基礎理論研究代表者以外ソフトウェア / 理工系 / 小区分60050:ソフトウェア関連 / ソフトウエア / 小区分62040:エンタテインメントおよびゲーム情報学関連 / 合同審査対象区分:小区分60010:情報学基礎論関連、小区分60020:数理情報学関連 / 小区分60020:数理情報学関連 / 小区分60010:情報学基礎論関連 / 計算機科学 / 情報学基礎
キーワード	研究代表者カット除去 / ラムダ計算 / 合流性 / シーケント計算 / 古典論理 / 帰納的述語 / 分離論理 / 型検査 / 存在型 / 強正規化可能性 … もっと見る / 置換簡約 / CPS変換 / 強正規化性 / カリーハワード同型 / 証明体系 / 不動点演算子 / カット除去可能性 / 循環証明体系 / ソフトウェア検証 / 証明論 / 循環証明 / カット除去定理 / 交叉型 / ラムダ・ミュー計算 / ストリーム / プログラミング言語のモデル / 型システム / ストリーム計算 / 書き換え系 / ドメインフリー / 決定不可能性 / 型付け可能性問題 / 型推論問題 / 型検査問題 / 多相型 / 決定可能性 / 型理論 / 証明正規化 / 自然演出繹 / 一般除去規則 / 決定問題 / 型推論 / 自然演繹 / コントロールオペレータ … もっと見る研究代表者以外型理論 / メタ言語 / プログラミング言語 / ソフトウェア検証 / 抽象操作 / 並行計算モデル / トレース意味論 / 計算効果 / メタ理論 / 式の理論 / ソフトウェア開発 / 自然枠組 / 限定継続 / 文脈 / 変数の衝突 / 超変数 / 文法的対象 / 対象言語 / テンポと拍子の取得 / MIDI演奏 / 生成音楽理論 / 演奏への表情付け / MIDI解析 / トークン / MIDIイベントのトークン化 / リズム量子化 / 自動採譜 / SMTソルバー / Assume-Gurantee / 時間付並行逆計算 / 到達可能性解析 / 分割検証 / アクティブ学習アルゴリズム / イベントクロックオートマトン / 拡張有限状態オートマトン / Assume-Gurantee検証 / 頑健性 / アクティブ学習 / 循環証明 / 到達可能性 / 実行時エラー検証 / プログラム変換 / 論理制約付き項書換えシステム / メモリ安全性 / 分離論理 / ソフトウェア解析 / 非決定計算 / 顕在的契約計算 / 型システム / 漸進的型付け / 逆計算 / ソフトウェアデバッグ / ソフトウエア学 / 実時間性 / 計算モデル / 並行プログラミング言語 / 離散時間モデル / デバッグモデル / 並行計算 / 因果無矛盾性 / 構造操作意味規則 / バックトラック逆計算 / 逆計算モデル / 通信プロセスモデル / 通信プロセス計算 / 実時間プログラム / 逆方向計算 / 逆方向デバッグ技法 / 可逆抽象機械 / 可逆計算実行環境 / 可逆デバッガ / 可逆実行環境 / 並行プログラム / 可逆計算 / Context / Variable Collision / Meta Variable / Syntactic Object / Meta Language / Object Language / 計算体系 / 強正規化性 / 合流性 / 環境 / shift/reset / ゲーム意味論 / 代入 / プログラム検証 / ソフトウェア契約 / イタリア / シンガポール / 国際情報交換 / 存在型 / 項書換 / ソフトウェアの安全性 / クラス理論 / メタ変数 / 明示的環境 / 線形時間時相論理 / 環境適応型ソフトウェア / Natural Framework / 変数参照 / 表現の理論 / 合成規則 / 明示的代入 / 導出 / 判断 / α同値性 / 具体化操作 / 表現理論隠す

論理制約付き項書換えに関する余帰納法に基づくプログラム検証法の開発
- 研究代表者
  
  西田直樹
- 研究期間 (年度)
  2024 – 2028
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60010:情報学基礎論関連
   小区分60020:数理情報学関連
   合同審査対象区分:小区分60010:情報学基礎論関連、小区分60020:数理情報学関連
- 研究機関
  名古屋大学
循環証明体系におけるカット除去定理とカット規則の制限研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2022 – 2025
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
分離論理を用いたソフトウェア検証の発展
- 研究代表者
  
  龍田真
- 研究期間 (年度)
  2021 – 2023
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  国立情報学研究所
データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法
- 研究代表者
  
  結縁祥治
- 研究期間 (年度)
  2021 – 2025
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  名古屋大学
形式言語理論に基づく自動採譜
- 研究代表者
  
  酒井正彦
- 研究期間 (年度)
  2020 – 2024
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分62040:エンタテインメントおよびゲーム情報学関連
- 研究機関
  名古屋大学
循環証明体系の証明論的分析研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2018 – 2020
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル
- 研究代表者
  
  結縁祥治
- 研究期間 (年度)
  2017 – 2020
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウェア
- 研究機関
  名古屋大学
現代的なプログラミング言語のための漸進的型システムの理論
- 研究代表者
  
  五十嵐淳
- 研究期間 (年度)
  2017 – 2020
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウェア
- 研究機関
  京都大学
計算における無限概念と古典論理研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2015 – 2017
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  情報学基礎理論
- 研究機関
  名古屋大学
ソフトウェア契約に基づく高階型付プログラムの理論
- 研究代表者
  
  五十嵐淳
- 研究期間 (年度)
  2013 – 2016
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウェア
- 研究機関
  京都大学
ストリーム計算のための計算モデル研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2012 – 2014
- 研究種目
  
  若手研究(B)
- 研究分野
  
  情報学基礎
- 研究機関
  京都大学
存在型の型理論
- 研究代表者
  
  龍田真
- 研究期間 (年度)
  2011 – 2014
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  情報学基礎
- 研究機関
  国立情報学研究所
バグのないソフトウェア構築環境に関する研究の新展開
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2010 – 2012
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウエア
- 研究機関
  京都大学
二階存在量化子をもつ計算体系研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2009 – 2011
- 研究種目
  
  若手研究(B)
- 研究分野
  
  情報学基礎
- 研究機関
  京都大学
計算と論理の融合によるバグのないソフトウェア構築環境に関する研究
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2007 – 2009
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウエア
- 研究機関
  京都大学
安全・安心な環境適応型ソフトウェアの基礎理論に関する研究
- 研究代表者
  
  五十嵐淳
- 研究期間 (年度)
  2006
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  京都大学
古典論理の構文論的双対性とその計算論的意味研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2006 – 2008
- 研究種目
  
  若手研究(B)
- 研究分野
  
  情報学基礎
- 研究機関
  京都大学
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2004 – 2005
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  京都大学
古典論理に基づく非決定的計算体系研究代表者
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2004 – 2005
- 研究種目
  
  若手研究(B)
- 研究分野
  
  情報学基礎
- 研究機関
  京都大学
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2003
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  京都大学
環境と文脈を持つ計算体系とその論理
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2001 – 2003
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  京都大学

[雑誌論文] Cut-elimination for cyclic proof systems with inductively defined propositions2022
- 著者名/発表者名
  Daisuke Kimura, Koji Nakazawa, and Kenji Saotome
- 雑誌名
  
  RIMS Kokyuroku
  
  巻: 2228 ページ: 30-40
- オープンアクセス
- データソース
  KAKENHI-PROJECT-22K11901
[雑誌論文] Biabduction for Separation Logic with Arrays and Lists2022
- 著者名/発表者名
  Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, oji Nakazawa, and Mirai Ikebuchi
- 雑誌名
  
  Biabduction for Separation Logic with Arrays and Lists
  
  巻: 1
- 査読あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-21H03421
[雑誌論文] Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions2021
- 著者名/発表者名
  Saotome, Kenji ; Nakazawa, Koji ; Kimura, Daisuke
- 雑誌名
  
  6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021,
  
  巻: LIPIcs 195
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-23K21654
[雑誌論文] Function Pointer Eliminator for C Programs2021
- 著者名/発表者名
  Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa
- 雑誌名
  
  Lecture Notes in Computer Science
  
  巻: 13008 ページ: 23-37
- DOI
  10.1007/978-3-030-89051-3_2
- ISBN
  9783030890506, 9783030890513
- 査読あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-18H03226, KAKENHI-PROJECT-21H03421
[雑誌論文] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020
- 著者名/発表者名
  Saotome Kenji、Nakazawa Koji、Kimura Daisuke
- 雑誌名
  
  FLOPS 2020, Lecture Notes in Computer Science
  
  巻: 12073 ページ: 88-105
- DOI
  10.1007/978-3-030-59025-3_6
- ISBN
  9783030590246, 9783030590253
- 査読あり
- データソース
  KAKENHI-PROJECT-18K11161
[雑誌論文] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020
- 著者名/発表者名
  KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
- 雑誌名
  
  コンピュータソフトウェア
  
  巻: 37 号: 1 ページ: 1_39-1_52
- DOI
  10.11309/jssst.37.1_39
- NAID
  130007815024
- ISSN
  0289-6540
- 年月日
  2020-01-24
- 言語
  日本語
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
[雑誌論文] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019
- 著者名/発表者名
  Tatsuta Makoto、Nakazawa Koji、Kimura Daisuke
- 雑誌名
  
  LNCS (APLAS 2019)
  
  巻: 11893 ページ: 367-387
- DOI
  10.1007/978-3-030-34175-6_19
- ISBN
  9783030341749, 9783030341756
- 査読あり
- データソース
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-17H01722
[雑誌論文] Compositional Z: Confluence proofs for permutative conversion2016
- 著者名/発表者名
  Koji Nakazawa and Ken-etsu Fujita
- 雑誌名
  
  Studia Logica
  
  巻: 104 号: 6 ページ: 1205-1224
- DOI
  10.1007/s11225-016-9673-0
- NAID
  120005971246
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-15K00012
[雑誌論文] {高階契約を持つプログラミング言語に対するトレース意味論2015
- 著者名/発表者名
  村井涼, 中澤巧爾, 五十嵐淳
- 雑誌名
  
  第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)論文集
  
  巻: 1
- データソース
  KAKENHI-PROJECT-25280024
[雑誌論文] Reduction system for extensional lambda-mu calculus2014
- 著者名/発表者名
  Koji Nakazawa and Tomoharu Nagai
- 雑誌名
  
  Lecture Notes in Computer Science
  
  巻: 8560 ページ: 340-363
- DOI
  10.1007/978-3-319-08918-8_24
- ISBN
  9783319089171, 9783319089188
- 査読あり
- データソース
  KAKENHI-PROJECT-24700011
[雑誌論文] Confluence for classical logic through the distinction between values and computation2014
- 著者名/発表者名
  Jose Espirito Santo, Ralph Matthes, Koji Nakazawa, and Luis Pinto
- 雑誌名
  
  Electric Proceedings in Theoretical Computer Science
  
  巻: 164 ページ: 63-77
- DOI
  10.4204/eptcs.164.5
- 査読あり
- データソース
  KAKENHI-PROJECT-24700011
[雑誌論文] Type checking and typability in domain-free lambda calculi2011
- 著者名/発表者名
  Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
- 雑誌名
  
  Theoretical Computer Science
  
  巻: 412(44) ページ: 6193-6207
- データソース
  KAKENHI-PROJECT-21700013
[雑誌論文] Type checking and typability in domain-free lambda calculi2011
- 著者名/発表者名
  K.Nakazawa, M.Tatsuta, Y.Kameyama, H.Nakano
- 雑誌名
  
  Theoretical Computer Science
  
  巻: 412(44) 号: 44 ページ: 6193-6207
- DOI
  10.1016/j.tcs.2011.06.020
- 査読あり
- データソース
  KAKENHI-PROJECT-22300008, KAKENHI-PROJECT-23650003
[雑誌論文] Type checking and inference are equivalent in lambda calculi with existential types2010
- 著者名/発表者名
  Yuki Kato and Koji Nakazawa
- 雑誌名
  
  18th International Workshop on Functional and(Constraint) Logic Programming(WFLP 2009)
  
  巻: 5979 ページ: 96-110
- データソース
  KAKENHI-PROJECT-21700013
[雑誌論文] Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems. Chicago Journal of Theoretical Computer Science2010
- 著者名/発表者名
  Koji Nakazawa and Makoto Tatsuta
- 雑誌名
  
  Special Issue : Selected papers from 2009 Computing : The Australasian Theory Symposium(CATS2009)
  
  巻: 7
- データソース
  KAKENHI-PROJECT-21700013
[雑誌論文] Type Checking and Inference for Polymorphic and Existential Types.2009
- 著者名/発表者名
  Koji Nakazawa and Makoto Tatsuta
- 雑誌名
  
  Computing : The Australasian Theory Symposium (CATS2009) (CD-ROM)
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Type Checking and Inference for Polymorphic and Existential Types2009
- 著者名/発表者名
  K. Nakazawa and M. Tatsuta
- 雑誌名
  
  Computing : The Australasian Theory Symposium (CATS'09) (CD-ROM)
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence.2008
- 著者名/発表者名
  Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
- 雑誌名
  
  Computer Science Logic (CSL' 08), Lecture Notes in Computer Science 5213
  
  ページ: 478-492
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence2008
- 著者名/発表者名
  K. Nakazawa, M. Tatsuta, Y. Kameyama, and H. Nakano
- 雑誌名
  
  Computer Science Logic (CSL'09)
  
  ページ: 478-492
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Strong normalization of classical natural deduction with disjunctions2008
- 著者名/発表者名
  Koji Nakazawa and Makoto Tatsuta
- 雑誌名
  
  Annals of Pure and Applied Logic 153
  
  ページ: 21-37
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Strong Normalization of Classical Natural Deduction with Disjunctns2008
- 著者名/発表者名
  Koji Nakazawa and Makoto Tatsuta
- 雑誌名
  
  Annals of Pure and Applied Logic 153
  
  ページ: 21-37
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] An isomorphism between cut-elimination procedure and proof reduction2007
- 著者名/発表者名
  Koji Nakazawa
- 雑誌名
  
  Typed Lambda Calculi and Applications (TLCA'07) (To appear)
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] An Isomorphism Between Cut-Elimination Procedure and Proof Reduction2007
- 著者名/発表者名
  Koji Nakazawa
- 雑誌名
  
  Typed Lambda Calculi and Applications (TLCA2007)
  
  ページ: 336-350
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] An Isomorphism between Cut-Elimination Procedure and Proof Reduction2007
- 著者名/発表者名
  Koji Nakazawa
- 雑誌名
  
  Typed Lambda Calculi and Applications (TLCA' 07), Lecture Notes in Computer Science 4583
  
  ページ: 336-350
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] Strong normalization proofs by CPS-translations2006
- 著者名/発表者名
  Satoshi Ikeda, Koji Nakazawa
- 雑誌名
  
  Information Processing Letters 99
  
  ページ: 163-170
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] 選言を含む自然演繹古典論理の強正規化性2006
- 著者名/発表者名
  中澤巧爾, 龍田真
- 雑誌名
  
  第8回プログラミング言語およびプログラミング言語ワークショップ(PPL2006)論文集
  
  ページ: 187-202
- データソース
  KAKENHI-PROJECT-16016245
[雑誌論文] 選言を含む自然演繹古典論理の強正規化性2006
- 著者名/発表者名
  中澤巧爾, 龍田真
- 雑誌名
  
  第8回プログラミング言語およびプログラミング言語ワークショップ(PPL2006)論文集
  
  ページ: 187-202
- データソース
  KAKENHI-PROJECT-16700012
[雑誌論文] Strong normalization proofs by CPS-translations2006
- 著者名/発表者名
  Satoshi Ikeda, Koji Nakazawa
- 雑誌名
  
  Information Processing Letters 99
  
  ページ: 163-170
- データソース
  KAKENHI-PROJECT-18049044
[雑誌論文] Strong Normalization Proofs by CPS-Translations2006
- 著者名/発表者名
  Satoshi Ikeda and Koji Nakazawa
- 雑誌名
  
  Information Processing Letters 99
  
  ページ: 163-170
- 査読あり
- データソース
  KAKENHI-PROJECT-18700008
[雑誌論文] コントロールオペレータをもつ計算体系の強正規化可能性のCPS変換を用いた証明2005
- 著者名/発表者名
  池田聡, 中澤巧爾
- 雑誌名
  
  第7回プログラミング言語およびプログラミング言語ワークショップ(PPL2005)論文集
  
  ページ: 171-186
- データソース
  KAKENHI-PROJECT-16700012
[学会発表] 不動点演算子を持つ命題論理に対する循環証明体系のカット無し完全性2024
- 著者名/発表者名
  堀弘昌, 中澤巧爾, 龍田真
- 学会等名
  第26回プログラミングおよびプログラミング言語ワークショップ
- データソース
  KAKENHI-PROJECT-22K11901
[学会発表] 不動点演算子を持つ命題論理に対する循環証明体系のカット無し完全性2024
- 著者名/発表者名
  堀弘昌, 中澤巧爾, 龍田真
- 学会等名
  第26回プログラミングおよびプログラミング言語ワークショップ (PPL2024) ポスター
- データソース
  KAKENHI-PROJECT-23K21654
[学会発表] 循環証明とカット除去2023
- 著者名/発表者名
  中澤巧爾, 早乙女献自
- 学会等名
  計算・言語・論理の研究集会 2023
- データソース
  KAKENHI-PROJECT-22K11901
[学会発表] Decidable entailment checking for concurrent separation logic with fractional permissions2022
- 著者名/発表者名
  Yeonseok Lee and Koji Nakazawa
- 学会等名
  日本ソフトウェア科学会第39回大会
- データソース
  KAKENHI-PROJECT-22K11901
[学会発表] 命題論理に対する無限証明体系と循環証明体系の証明能力同等性2022
- 著者名/発表者名
  堀弘昌, 中澤巧爾, 龍田真
- 学会等名
  日本数学会秋季総合分科会
- データソース
  KAKENHI-PROJECT-22K11901
[学会発表] 分離論理における記号ヒープのための循環証明体系におけるカットの制限について2020
- 著者名/発表者名
  早乙女献自，中澤巧爾，木村大輔
- 学会等名
  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] 古典論理に対する汎用的自然演繹の証明正規化2020
- 著者名/発表者名
  福井康介, 中澤巧爾, 石井沙織, 結縁祥治
- 学会等名
  第22回プログラミングおよびプログラミング言語ワークショップ
- データソース
  KAKENHI-PROJECT-17H01723
[学会発表] Failure of cut-elimination in cyclic proofs of separation logic2019
- 著者名/発表者名
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
- 学会等名
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] Spatial factorization in cyclic-proof system for separation logic2019
- 著者名/発表者名
  Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura
- 学会等名
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] On cut elimination in cyclic-proof systems2019
- 著者名/発表者名
  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome
- 学会等名
  3rd Workshop on Mathamatical Logic and Its Applications (MLA 2019)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] プログラムの正しさを証明する---分離論理入門---2019
- 著者名/発表者名
  中澤巧爾
- 学会等名
  日本数学会2019年度年会
- 招待講演
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] 循環証明体系における準カット除去可能性について2019
- 著者名/発表者名
  早乙女献自，中澤巧爾
- 学会等名
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] Completeness of cyclic proofs for symbolic heaps with inductive definitions2019
- 著者名/発表者名
  Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura
- 学会等名
  The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-17H01723
[学会発表] 高階契約に対するトレース意味論の完全抽象性2018
- 著者名/発表者名
  井上鉄也，中澤巧爾
- 学会等名
  第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
- データソース
  KAKENHI-PROJECT-17H01722
[学会発表] 高階契約に対するトレース意味論の完全抽象性2018
- 著者名/発表者名
  井上鉄也，中澤巧爾
- 学会等名
  第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
- データソース
  KAKENHI-PROJECT-17H01723
[学会発表] 帰納的述語を含む分離論理によるプログラム検証のためのループ不変式の導出2018
- 著者名/発表者名
  仲田壮佑，中澤巧爾
- 学会等名
  第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
- データソース
  KAKENHI-PROJECT-17H01722
[学会発表] Z for call-by-value2017
- 著者名/発表者名
  Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa
- 学会等名
  6th International Workshop on Cofluence (IWC 2017)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] Z for call-by-value2017
- 著者名/発表者名
  Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa
- 学会等名
  6th International Workshop on Cofluence (IWC 2017)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-17H01722
[学会発表] Characterizing trees for lambda-mu terms2016
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  8th International Workshop on Higher-Order Rewriting (HOR 2016)
- 発表場所
  ポルト，ポルトガル
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] Church-Rosser theorem and compositional Z-property2016
- 著者名/発表者名
  Ken-etsu Fujita and Koji Nakazawa
- 学会等名
  日本ソフトウェア科学会第33回大会
- 発表場所
  東北大学
- 年月日
  2016-09-06
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] Intersection and Union Type Assignment and Polarised lambda-bar-mu-mu-tilde2016
- 著者名/発表者名
  Takeshi Tsukada and Koji Nakazawa
- 学会等名
  第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
- 発表場所
  岡山
- 年月日
  2016-03-08
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] A Denotational Semantics of a Probabilistic Stream-Processing Language2016
- 著者名/発表者名
  Yohei Miyamoto, Kohei Suenaga, and Koji Nakazawa
- 学会等名
  Workshop on Probabilistic Programming Semantics (PPS 2016)
- 発表場所
  St. Petersburg, FL, USA
- 年月日
  2016-01-23
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-25280024
[学会発表] Lambda Calculi and Confluence from A to Z2015
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  4th International Workshop on Confluence (IWC2015)
- 発表場所
  Berlin
- 年月日
  2015-08-02
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] Compositional Z: Confluence Proofs for Permutative Conversion2015
- 著者名/発表者名
  Koji Nakazawa and Ken-etsu Fujita
- 学会等名
  第32回日本ソフトウェア科学会大会
- 発表場所
  東京
- 年月日
  2015-09-10
- データソース
  KAKENHI-PROJECT-15K00012
[学会発表] Compositional Z: Confluence Proofs for Permutative Conversion2015
- 著者名/発表者名
  Koji Nakazawa, Ken-etsu Fujita
- 学会等名
  第32回日本ソフトウェア科学会大会
- 発表場所
  早稲田大学（東京都新宿区）
- 年月日
  2015-09-08
- データソース
  KAKENHI-PROJECT-25280024
[学会発表] Lambda Calculi and Confluence from A to Z2015
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  4th International Workshop on Confluence (IWC2015)
- 発表場所
  Berlin, Germany
- 年月日
  2015-08-02
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-25280024
[学会発表] Extensional models of typed lambda-mu calculus2014
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  The Fifth International Workshop on Classical Logic and Computation (CL&C'14)
- 発表場所
  オーストリア、ウィーン
- 年月日
  2014-07-13
- データソース
  KAKENHI-PROJECT-24700011
[学会発表] 契約つきモジュール計算のトレース意味論に向けて2014
- 著者名/発表者名
  村井涼, 五十嵐淳, 中澤巧爾
- 学会等名
  第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
- 発表場所
  熊本県阿蘇市
- データソース
  KAKENHI-PROJECT-25280024
[学会発表] 外延的Λμ計算に対する簡約関係2014
- 著者名/発表者名
  永井智映，中澤巧爾
- 学会等名
  第16回プログラミングおよびプログラミング言語ワークショップ (PPL2014)
- 発表場所
  熊本県阿蘇市
- データソース
  KAKENHI-PROJECT-24700011
[学会発表] Extensional Models of Untyped Lambda-mu Calculus2012
- 著者名/発表者名
  Koji Nakazawa and Shin-ya Katsumata
- 学会等名
  Fourth International Workshop on Classical Logic and Computation (CL&C'12)
- 発表場所
  Warwick, England
- データソース
  KAKENHI-PROJECT-24700011
[学会発表] 多相型と存在型に対する型検査問題の同値性2011
- 著者名/発表者名
  加藤祐輝, 中澤巧爾
- 学会等名
  第13回プログラミングおよびプログラミング言語ワークショップ(PPL2011)ポスター発表
- 発表場所
  札幌
- 年月日
  2011-03-09
- データソース
  KAKENHI-PROJECT-21700013
[学会発表] 多相型と存在型に対する型検査問題の同値性2011
- 著者名/発表者名
  加藤祐輝, 中澤巧爾
- 学会等名
  第13回プログラミングおよびプログラミング言語ワークショップ
- 発表場所
  札幌
- データソース
  KAKENHI-PROJECT-21700013
[学会発表] Continuations and classical logic : using continuations as a tool for classical logic2011
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  ACM SIGPLAN Continuation Workshop
- 発表場所
  Tokyo
- 年月日
  2011-09-24
- データソース
  KAKENHI-PROJECT-21700013
[学会発表] 多相型と存在型に対する型検査問題の同値性2011
- 著者名/発表者名
  加藤祐輝, 中澤巧爾
- 学会等名
  第13回プログラミングおよびプログラミング言語ワークショップ(PPL2011)
- 発表場所
  北海道札幌市
- 年月日
  2011-03-09
- データソース
  KAKENHI-PROJECT-22300008
[学会発表] 古典シークエント計算の強正規化可能性の構文論的証明2010
- 著者名/発表者名
  山口洋平, 中澤巧爾
- 学会等名
  第12回プログラミングおよびプログラミング言語ワークショップPPL2010(ショートプレゼンテーション)
- 発表場所
  香川県琴平
- 年月日
  2010-03-04
- データソース
  KAKENHI-PROJECT-21700013
[学会発表] Type checking and inference are equivalent in lambda calculi with existential types2009
- 著者名/発表者名
  Yuki Kato and Koji Nakazawa
- 学会等名
  18^(th) International Workshop on Functional and(Constraint) Logic Programming
- 発表場所
  Brasilia, Brazil
- データソース
  KAKENHI-PROJECT-21700013
[学会発表] 存在型に対する型検査問題と型推論問題の同値性2009
- 著者名/発表者名
  加藤祐輝, 中澤巧爾
- 学会等名
  第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), ポスター
- データソース
  KAKENHI-PROJECT-18700008
[学会発表] trong Cut-Elimination and CPS-Translations. (In T. Kutsia and M. Marin, eds.)2007
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  Austria-Japan Workshop on Symbolic Computation and Software Verification, No. 07-09 in RISC-Linz Report Series,
- データソース
  KAKENHI-PROJECT-18700008
[学会発表] An Isomorphism between Cut-Elimination Procedure and Proof Reduction2007
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  SCORE Summer Workshop on Symbolic Computation and Software Verification
- データソース
  KAKENHI-PROJECT-18700008
[学会発表] Confluence for lambda calculi with permutative conversion
- 著者名/発表者名
  Koji Nakazawa
- 学会等名
  42nd TRS meeting
- 発表場所
  東京都中央区
- 年月日
  2015-02-07 – 2015-02-09
- データソース
  KAKENHI-PROJECT-24700011
[学会発表] {高階契約を持つプログラミング言語に対するトレース意味論
- 著者名/発表者名
  村井涼, 中澤巧爾, 五十嵐淳
- 学会等名
  第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)
- 発表場所
  愛媛県松山市道後プリンスホテル
- 年月日
  2015-03-04 – 2015-03-06
- データソース
  KAKENHI-PROJECT-25280024
[学会発表] 置換簡約を含むラムダ計算の合流性
- 著者名/発表者名
  中澤巧爾, 藤田憲悦
- 学会等名
  第17回プログラミングおよびプログラミング言語ワークショップ
- 発表場所
  愛媛県松山市
- 年月日
  2015-03-04 – 2015-03-06
- データソース
  KAKENHI-PROJECT-24700011

1. 五十嵐淳 (40323456)

共同の研究課題数: 6件

共同の研究成果数: 3件
2. 佐藤雅彦 (20027387)

共同の研究課題数: 6件

共同の研究成果数: 1件
3. 亀山幸義 (10195000)

共同の研究課題数: 4件

共同の研究成果数: 0件
4. 桜井貴文 (60183373)

共同の研究課題数: 3件

共同の研究成果数: 0件
5. 木村大輔 (90455197)

共同の研究課題数: 3件

共同の研究成果数: 8件
6. 山本章博 (30230535)

共同の研究課題数: 2件

共同の研究成果数: 0件
7. 湯淺太一 (60158326)

共同の研究課題数: 2件

共同の研究成果数: 0件
8. 龍田真 (80216994)

共同の研究課題数: 2件

共同の研究成果数: 2件
9. 結縁祥治 (70230612)

共同の研究課題数: 2件

共同の研究成果数: 0件
10. 馬谷誠二 (40378831)

共同の研究課題数: 2件

共同の研究成果数: 0件
11. 西田直樹 (00397449)

共同の研究課題数: 2件

共同の研究成果数: 0件
12. 関浩之 (80196948)

共同の研究課題数: 2件

共同の研究成果数: 0件
13. 末永幸平 (70633692)

共同の研究課題数: 1件

共同の研究成果数: 1件
14. 竹内泉 (20264583)

共同の研究課題数: 1件

共同の研究成果数: 0件
15. 海野広志 (80569575)

共同の研究課題数: 1件

共同の研究成果数: 0件
16. 松原豊 (30547500)

共同の研究課題数: 1件

共同の研究成果数: 0件
17. 小川瑞史 (40362024)

共同の研究課題数: 1件

共同の研究成果数: 0件
18. 今井敬吾 (70456630)

共同の研究課題数: 1件

共同の研究成果数: 0件
19. 酒井正彦 (50215597)

共同の研究課題数: 1件

共同の研究成果数: 0件
20. 東条敏 (90272989)

共同の研究課題数: 1件

共同の研究成果数: 0件

中澤 巧爾 Nakazawa Koji

研究課題

研究成果

共同研究者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

循環証明体系におけるカット除去定理とカット規則の制限研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

循環証明体系の証明論的分析研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

計算における無限概念と古典論理研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

ストリーム計算のための計算モデル研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

二階存在量化子をもつ計算体系研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

研究代表者

中澤巧爾 Nakazawa Koji