Nakazawa Koji 中澤巧爾

… Alternative Names

NAKAZAWA Koji 中澤巧爾

Less

Researcher Number	80362581
Other IDs
Affiliation (Current)	2025: 名古屋大学, 情報学研究科, 准教授
Affiliation (based on the past Project Information) *help	2017 – 2024: 名古屋大学, 情報学研究科, 准教授 2015 – 2016: 名古屋大学, 情報科学研究科, 准教授 2007 – 2014: Kyoto University, 情報学研究科, 助教 2011 – 2012: 京都大学, 大学院・情報学研究科, 助教 2008 – 2009: Kyoto University, 大学院・情報学研究科, 助教 2003 – 2006: Kyoto University, Graduate School of Informatics, Research Associate, 情報学研究科, 助手
Review Section/Research Field	Principal Investigator Fundamental theory of informatics / Basic Section 60010:Theory of informatics-related / Theory of informatics Except Principal Investigator Software / Science and Engineering / Basic Section 60050:Software-related / Software / Basic Section 62040:Entertainment and game informatics-related / Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related / Basic Section 60020:Mathematical informatics-related / Basic Section 60010:Theory of informatics-related / 計算機科学 / Fundamental theory of informatics
Keywords	Principal Investigator カット除去 / ラムダ計算 / 合流性 / シーケント計算 / 古典論理 / 帰納的述語 / 分離論理 / 型検査 / 存在型 / 強正規化可能性 … More / 置換簡約 / CPS変換 / 強正規化性 / カリーハワード同型 / 証明体系 / 不動点演算子 / カット除去可能性 / 循環証明体系 / ソフトウェア検証 / 証明論 / 循環証明 / カット除去定理 / 交叉型 / ラムダ・ミュー計算 / ストリーム / プログラミング言語のモデル / 型システム / ストリーム計算 / 書き換え系 / ドメインフリー / 決定不可能性 / 型付け可能性問題 / 型推論問題 / 型検査問題 / 多相型 / 決定可能性 / 型理論 / 証明正規化 / 自然演出繹 / 一般除去規則 / 決定問題 / 型推論 / 自然演繹 / コントロールオペレータ … More Except Principal Investigator 型理論 / メタ言語 / プログラミング言語 / ソフトウェア検証 / 抽象操作 / 並行計算モデル / トレース意味論 / 計算効果 / メタ理論 / 式の理論 / ソフトウェア開発 / 自然枠組 / 限定継続 / 文脈 / 変数の衝突 / 超変数 / 文法的対象 / 対象言語 / テンポと拍子の取得 / MIDI演奏 / 生成音楽理論 / 演奏への表情付け / MIDI解析 / トークン / MIDIイベントのトークン化 / リズム量子化 / 自動採譜 / SMTソルバー / Assume-Gurantee / 時間付並行逆計算 / 到達可能性解析 / 分割検証 / アクティブ学習アルゴリズム / イベントクロックオートマトン / 拡張有限状態オートマトン / Assume-Gurantee検証 / 頑健性 / アクティブ学習 / 循環証明 / 到達可能性 / 実行時エラー検証 / プログラム変換 / 論理制約付き項書換えシステム / メモリ安全性 / 分離論理 / ソフトウェア解析 / 非決定計算 / 顕在的契約計算 / 型システム / 漸進的型付け / 逆計算 / ソフトウェアデバッグ / ソフトウエア学 / 実時間性 / 計算モデル / 並行プログラミング言語 / 離散時間モデル / デバッグモデル / 並行計算 / 因果無矛盾性 / 構造操作意味規則 / バックトラック逆計算 / 逆計算モデル / 通信プロセスモデル / 通信プロセス計算 / 実時間プログラム / 逆方向計算 / 逆方向デバッグ技法 / 可逆抽象機械 / 可逆計算実行環境 / 可逆デバッガ / 可逆実行環境 / 並行プログラム / 可逆計算 / Context / Variable Collision / Meta Variable / Syntactic Object / Meta Language / Object Language / 計算体系 / 強正規化性 / 合流性 / 環境 / shift/reset / ゲーム意味論 / 代入 / プログラム検証 / ソフトウェア契約 / イタリア / シンガポール / 国際情報交換 / 存在型 / 項書換 / ソフトウェアの安全性 / クラス理論 / メタ変数 / 明示的環境 / 線形時間時相論理 / 環境適応型ソフトウェア / Natural Framework / 変数参照 / 表現の理論 / 合成規則 / 明示的代入 / 導出 / 判断 / α同値性 / 具体化操作 / 表現理論 Less

Development of Program Verification Techniques Based on Coinduction on Logically Constrained Rewriting
- Principal Investigator
  
  西田直樹
- Project Period (FY)
  2024 – 2028
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
  Basic Section 60020:Mathematical informatics-related
  Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related
- Research Institution
  Nagoya University
循環証明体系におけるカット除去定理とカット規則の制限Principal Investigator
- Principal Investigator
  
  中澤巧爾
- Project Period (FY)
  2022 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
分離論理を用いたソフトウェア検証の発展
- Principal Investigator
  
  龍田真
- Project Period (FY)
  2021 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Informatics
A design of automaton network with data and time based on a compositional active learning
- Principal Investigator
  
  結縁祥治
- Project Period (FY)
  2021 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Nagoya University
Automated transcription based on formal language theory
- Principal Investigator
  
  酒井正彦
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 62040:Entertainment and game informatics-related
- Research Institution
  Nagoya University
Proof theoretic analysis of cyclic proof systemsPrincipal Investigator
- Principal Investigator
  
  Nakazawa Koji
- Project Period (FY)
  2018 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
A reversible debugging model for real-time concurrent programs
- Principal Investigator
  
  YUEN SHOJI
- Project Period (FY)
  2017 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Nagoya University
Theory of Gradual Typing for Modern Programming Languages
- Principal Investigator
  
  Atsushi Igarashi
- Project Period (FY)
  2017 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Kyoto University
Classical logic and infinite phenomena in computationPrincipal Investigator
- Principal Investigator
  
  Nakazawa Koji
- Project Period (FY)
  2015 – 2017
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Theory of informatics
- Research Institution
  Nagoya University
Theory of Higher-Order Typed Programs based Software Contracts
- Principal Investigator
  
  Igarashi Atsushi
- Project Period (FY)
  2013 – 2016
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Kyoto University
Mathematical models for stream computationPrincipal Investigator
- Principal Investigator
  
  NAKAZAWA Koji
- Project Period (FY)
  2012 – 2014
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Kyoto University
Type Theory of Existential Types
- Principal Investigator
  
  TATSUTA Makoto
- Project Period (FY)
  2011 – 2014
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  National Institute of Informatics
New development of research on bug-free software construction environment
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  2010 – 2012
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Kyoto University
Calculi with Second-Order Existential QuantifierPrincipal Investigator
- Principal Investigator
  
  NAKAZAWA Koji
- Project Period (FY)
  2009 – 2011
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Kyoto University
Software development environment based on integration of computation and logic
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  2007 – 2009
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Kyoto University
安全・安心な環境適応型ソフトウェアの基礎理論に関する研究
- Principal Investigator
  
  IGARASHI Atsushi
- Project Period (FY)
  2006
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Kyoto University
Syntactic Duality of Classical Logic and Its Computational AspectPrincipal Investigator
- Principal Investigator
  
  NAKAZAWA Koji
- Project Period (FY)
  2006 – 2008
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Kyoto University
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
- Principal Investigator
  
  佐藤雅彦
- Project Period (FY)
  2004 – 2005
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Kyoto University
古典論理に基づく非決定的計算体系Principal Investigator
- Principal Investigator
  
  中澤巧爾
- Project Period (FY)
  2004 – 2005
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Kyoto University
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  2003
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Kyoto University
Calculi and Logic of Environment and Context
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  2001 – 2003
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  計算機科学
- Research Institution
  Kyoto University

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

1. IGARASHI Atsushi (40323456)

# of Collaborated Projects: 6 results

# of Collaborated Products: 3 results
2. SATO Masahiko (20027387)

# of Collaborated Projects: 6 results

# of Collaborated Products: 1 results
3. 亀山幸義 (10195000)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
4. 桜井貴文 (60183373)

# of Collaborated Projects: 3 results

# of Collaborated Products: 0 results
5. 木村大輔 (90455197)

# of Collaborated Projects: 3 results

# of Collaborated Products: 8 results
6. YAMAMOTO Akihiro (30230535)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
7. YUASA Taiichi (60158326)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
8. TATSUTA Makoto (80216994)

# of Collaborated Projects: 2 results

# of Collaborated Products: 2 results
9. YUEN SHOJI (70230612)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
10. 馬谷誠二 (40378831)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
11. 西田直樹 (00397449)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
12. 関浩之 (80196948)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
13. 末永幸平 (70633692)

# of Collaborated Projects: 1 results

# of Collaborated Products: 1 results
14. 竹内泉 (20264583)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
15. 海野広志 (80569575)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
16. 松原豊 (30547500)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
17. 小川瑞史 (40362024)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
18. 今井敬吾 (70456630)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
19. 酒井正彦 (50215597)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
20. 東条敏 (90272989)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

Nakazawa Koji 中澤 巧爾

NAKAZAWA Koji 中澤 巧爾

Research Projects

Research Products

Co-Researchers

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

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

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Proof theoretic analysis of cyclic proof systemsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Classical logic and infinite phenomena in computationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Mathematical models for stream computationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Calculi with Second-Order Existential QuantifierPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Nakazawa Koji 中澤巧爾

NAKAZAWA Koji 中澤巧爾