KIKUCHI Kentaro 菊池健太郎

… Alternative Names

KIKUCHI Kentarou 菊池健太郎

Less

Researcher Number	40396528
Other IDs
Affiliation (Current)	2024: 東北大学, 電気通信研究所, 助教
Affiliation (based on the past Project Information) *help	2016 – 2022: 東北大学, 電気通信研究所, 助教 2004 – 2006: 東北大学, 電気通信研究所, 助手 2002 – 2003: 千葉大学, 理学部, 特別研究員(PD)
Review Section/Research Field	Principal Investigator 計算機科学 / Basic Section 60050:Software-related / Software / Fundamental theory of informatics Except Principal Investigator Basic Section 60050:Software-related / Theory of informatics / 計算機科学 / Science and Engineering
Keywords	Principal Investigator プログラム検証 / 書き換えシステム / プログラム理論 / 数理論理学 / 合流性 / 理論計算機科学 / 局所十分完全性 / 帰納的定理 / 完全性 / 明示的代入計算 … More / ラムダ計算 / 強正規化性 / カリーハワード対応 / カット除去手続き / シーケント計算 … More Except Principal Investigator ラムダ計算 / 停止性 / Haskell / 合流性 / 関数プログラム / 書替え系 / 関数プログラミング / プログラム理論 / 代数仕様 / 書換え系 / ソフトウェア科学 / 検証 / 数理論理学 / 直観主義論理 / minlog / 証明検証系 / α同値 / 古典論理 / balanced weak confluence / external reduction / normalizing strategy / negular preserving approximation / needed reduction / reduction system / 木オートマン / 逐次性 / 到達可能性 / リダクションの近以 / 構成子システム / 条件付き書き換え / リダクションの近似 / 優先順位付き書き換え / 書き換えシステム / プロトコル検証 / 近似木オートマトン / 変換パターン / バランス弱合流性 / 外延リダクション / 正規化戦略 / 正規保存近似 / 必須リダクション / リダクションシステム / 項書き換えシステム / 定理自動証明 / プログラム変換 / ソフトウェア検証 / 情報基礎 Less

Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting
- Principal Investigator
  
  浜名誠
- Project Period (FY)
  2020 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Gunma University
先進的な高階書き換え理論に基づく遅延評価関数型プログラムの検証Principal Investigator
- Principal Investigator
  
  菊池健太郎
- Project Period (FY)
  2019 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Tohoku University
古典論理に基づく計算系とその性質の検証
- Principal Investigator
  
  桜井貴文
- Project Period (FY)
  2017 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Theory of informatics
- Research Institution
  Chiba University
Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting TheoryPrincipal Investigator
- Principal Investigator
  
  KIKUCHI Kentaro
- Project Period (FY)
  2016 – 2018
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Software
- Research Institution
  Tohoku University
完備化に基づくプログラム自動変換の研究
- Principal Investigator
  
  TOYAMA Yoshihito
- Project Period (FY)
  2005
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Tohoku University
シーケント計算に基づく型システムの研究Principal Investigator
- Principal Investigator
  
  菊池健太郎
- Project Period (FY)
  2005 – 2006
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Tohoku University
Program verification method based on reduction approximations
- Principal Investigator
  
  TOYAMA Yoshihito
- Project Period (FY)
  2002 – 2005
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  計算機科学
- Research Institution
  Tohoku University
非古典論理によるソフトウェア記述へのアプローチPrincipal Investigator
- Principal Investigator
  
  菊池健太郎
- Project Period (FY)
  2002 – 2004
- Research Category
  
  Grant-in-Aid for JSPS Fellows
- Research Field
  
  計算機科学
- Research Institution
  Tohoku University
  Chiba University

All 2022 2021 2020 2019 2018 2017 2016 2006 2004

All Journal Article Presentation

[Journal Article] Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting2022
- Author(s)
  Kentaro Kikuchi
- Journal Title
  
  Proceedings of the 19th International Colloquium on Theoretical Aspects of Computing (ICTAC 2022)
  
  Volume: 13572 Pages: 255-271
- DOI
  10.1007/978-3-031-17715-6_17
- ISBN
  9783031177149, 9783031177156
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] A Proof Method for Local Sufficient Completeness of Term Rewriting Systems2021
- Author(s)
  Tomoki Shiraishi, Kentaro Kikuchi, Takahito Aoto
- Journal Title
  
  Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021)
  
  Volume: 12819 Pages: 386-404
- DOI
  10.1007/978-3-030-85315-0_22
- ISBN
  9783030853143, 9783030853150
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables2021
- Author(s)
  Kikuchi Kentaro, Aoto Takahito
- Journal Title
  
  Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020)
  
  Volume: 12561 Pages: 56-73
- DOI
  10.1007/978-3-030-68446-4_3
- ISBN
  9783030684457, 9783030684464
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems2021
- Author(s)
  Kentaro Kikuchi, Takahito Aoto
- Journal Title
  
  Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)
  
  Volume: 213
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] The System SOL version 20202020
- Author(s)
  Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju
- Journal Title
  
  Proceedings of the 9th International Workshop on Confluence
  
  Volume: IWC 2020 Pages: 81-81
- Data Source
  KAKENHI-PROJECT-20H04164
[Journal Article] Polymorphic computation systems: Theory and practice of confluence with call-by-value2020
- Author(s)
  Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi
- Journal Title
  
  Science of Computer Programming
  
  Volume: 187 Pages: 102322-102322
- DOI
  10.1016/j.scico.2019.102322
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00005, KAKENHI-PROJECT-17K00092, KAKENHI-PROJECT-19K11891, KAKENHI-PROJECT-20H04164
[Journal Article] 項書き換えシステムにおける局所十分完全性の証明法2020
- Author(s)
  白石智輝, 青戸等人, 菊池健太郎
- Journal Title
  
  第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集
  
  Volume: 22
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] The System SOL version 20202020
- Author(s)
  Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju
- Journal Title
  
  Proceedings of the 9th International Workshop on Confluence (IWC 2020)
  
  Volume: － Pages: 81-81
- Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K11891
[Journal Article] Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation2019
- Author(s)
  Kentaro Kikuchi, Takahito Aoto, Isao Sasano
- Journal Title
  
  Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)
  
  Volume: 21 Pages: 1-14
- DOI
  10.1145/3354166.3354178
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00005, KAKENHI-PROJECT-18K11158, KAKENHI-PROJECT-19K11891
[Journal Article] The System SOL version 20182018
- Author(s)
  Makoto Hamana, Kentaro Kikuchi
- Journal Title
  
  Proceedings of the 7th International Workshop on Confluence (IWC 2018)
  
  Volume: － Pages: 70-70
- Open Access
- Data Source
  KAKENHI-PROJECT-16K00091
[Journal Article] Confluence by Strong Commutation with Disjoint Parallel Reduction2017
- Author(s)
  Kentaro Kikuchi
- Journal Title
  
  Preproceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)
  
  Volume: -
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-16K00091
[Journal Article] Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems2017
- Author(s)
  Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
- Journal Title
  
  Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)
  
  Volume: 10483 Pages: 115-131
- DOI
  10.1007/978-3-319-66167-4_7
- ISBN
  9783319661667, 9783319661674
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K00091, KAKENHI-PROJECT-17K00005, KAKENHI-PROJECT-15K00003
[Journal Article] A Rule-Based Procedure for Equivariant Nominal Unification2016
- Author(s)
  Takahito Aoto and Kentaro Kikuchi
- Journal Title
  
  Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016)
  
  Volume: －
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K00091
[Journal Article] Nominal Confluence Tool2016
- Author(s)
  Takahito Aoto and Kentaro Kikuchi
- Journal Title
  
  Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)
  
  Volume: 9706 Pages: 173-182
- DOI
  10.1007/978-3-319-40229-1_12
- ISBN
  9783319402284, 9783319402291
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K00091
[Journal Article] Call-by-Name Reduction and Cut-Elimination in Classical Logic2006
- Author(s)
  Kentaro Kikuchi
- Journal Title
  
  Proceedings of the 1st International Workshop on Classical Logic and Computation
  
  Pages: 18-18
- Data Source
  KAKENHI-PROJECT-17700003
[Journal Article] On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus2006
- Author(s)
  Kentaro Kikuchi
- Journal Title
  
  Lecture Notes in Computer Science Vol. 4246
  
  Pages: 120-134
- Data Source
  KAKENHI-PROJECT-17700003
[Journal Article] Direct Proof of Strong Normalization for an Extended Herbelin's Calculus2004
- Author(s)
  Kentaro Kikuchi
- Journal Title
  
  Lecture Notes in Computer Science Vol.2998
  
  Pages: 244-259
- Data Source
  KAKENHI-PROJECT-02J02624
[Presentation] アトム変数を用いた名目単一化の実装2021
- Author(s)
  山上隼司, 菊池健太郎, 上野雄大, 大堀淳
- Organizer
  日本ソフトウェア科学会第38回大会
- Data Source
  KAKENHI-PROJECT-19K11891
[Presentation] 名目書き換えにおける強可換性を用いた合流性証明2020
- Author(s)
  菊池健太郎
- Organizer
  日本ソフトウェア科学会第37回大会
- Data Source
  KAKENHI-PROJECT-19K11891
[Presentation] 無限のデータを含む等式に対する帰納的定理証明2018
- Author(s)
  菊池健太郎, 篠埜功
- Organizer
  日本ソフトウェア科学会第35回大会
- Data Source
  KAKENHI-PROJECT-17K00005
[Presentation] 無限のデータを含む等式に対する帰納的定理証明2018
- Author(s)
  菊池健太郎, 篠埜功
- Organizer
  日本ソフトウェア科学会第35回大会
- Data Source
  KAKENHI-PROJECT-16K00091
[Presentation] ACPH: System Description for CoCo 20172017
- Author(s)
  Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
- Organizer
  The 6th International Workshop on Confluence (IWC 2017)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K00091
[Presentation] 完備化手続きにおける関数記号導入の戦略2016
- Author(s)
  伊藤佑太, 菊池健太郎, 外山芳人
- Organizer
  平成28年度電気関係学会東北支部連合大会
- Place of Presentation
  東北工業大学八木山キャンパス
- Year and Date
  2016-08-30
- Data Source
  KAKENHI-PROJECT-16K00091
[Presentation] ACPH: System Description for CoCo 20162016
- Author(s)
  Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
- Organizer
  The 5th International Workshop on Confluence (IWC 2016)
- Place of Presentation
  Obergurgl University Center, Austria
- Year and Date
  2016-09-08
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K00091
[Presentation] Nrbox: System Description for CoCo 20162016
- Author(s)
  Takahito Aoto and Kentaro Kikuchi
- Organizer
  The 5th International Workshop on Confluence (IWC 2016)
- Place of Presentation
  Obergurgl University Center, Austria
- Year and Date
  2016-09-08
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K00091

1. AOTO Takahito (00293390)

# of Collaborated Projects: 3 results

# of Collaborated Products: 6 results
2. TOYAMA Yoshihito (00251968)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
3. 草刈圭一郎 (90323112)

# of Collaborated Projects: 1 results

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

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
5. 浜名誠 (90334135)

# of Collaborated Projects: 1 results

# of Collaborated Products: 1 results
6. 室屋晃子 (00827454)

# of Collaborated Projects: 1 results

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

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

KIKUCHI Kentaro 菊池 健太郎

KIKUCHI Kentarou 菊池 健太郎

Research Projects

Research Products

Co-Researchers

Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting

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

Research Field

Research Institution

Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting TheoryPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

完備化に基づくプログラム自動変換の研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

シーケント計算に基づく型システムの研究Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Program verification method based on reduction approximations

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

非古典論理によるソフトウェア記述へのアプローチPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Journal Article] Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting2022

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] A Proof Method for Local Sufficient Completeness of Term Rewriting Systems2021

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables2021

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems2021

Author(s)

Journal Title

Data Source

[Journal Article] The System SOL version 20202020

Author(s)

Journal Title

Data Source

[Journal Article] Polymorphic computation systems: Theory and practice of confluence with call-by-value2020

KIKUCHI Kentaro 菊池健太郎

KIKUCHI Kentarou 菊池健太郎