研究者詳細

顔写真

キクチ　ケンタロウ
菊池　健太郎
Kentaro Kikuchi
所属
電気通信研究所　計算システム基盤研究部門　コンピューティング情報理論研究室
職名
助教
学位

  • 博士（情報科学） （北陸先端科学技術大学院大学）

e-Rad 研究者番号
40396528

研究分野 2

  • 情報通信 / ソフトウェア /

  • 情報通信 / 情報学基礎論 /

論文 43

  1. Characterizations of Partial Well-Behaved Lenses 査読有り

    Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi

    Proceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2025, Denver, CO, USA, 21 January 2025.　43-53　2025年

    出版者・発行元： ACM

    DOI： 10.1145/3704253.3706139 　

  2. Ground Confluence and Strong Commutation modulo Alpha-Equivalence in Nominal Rewriting 査読有り

    Kentaro Kikuchi

    Proceedings of the 19th International Colloquium on Theoretical Aspects of Computing (ICTAC 2022)　LNCS 13572　255-271　2022年

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-031-17715-6_17 　

  3. Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems 査読有り

    Kentaro Kikuchi, Takahito Aoto

    Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)　LIPIcs 213　49:1-49:15　2021年

    DOI： 10.4230/LIPIcs.FSTTCS.2021.49 　

  4. A Proof Method for Local Sufficient Completeness of Term Rewriting Systems 査読有り

    Tomoki Shiraishi, Kentaro Kikuchi, Takahito Aoto

    Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021)　LNCS 12819　386-404　2021年

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-030-85315-0_22 　

    ISSN：0302-9743

    eISSN：1611-3349

  5. Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables 査読有り

    Kentaro Kikuchi, Takahito Aoto

    Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020)　LNCS 12561　56-73　2021年

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-030-68446-4_3 　

    ISSN：0302-9743

    eISSN：1611-3349

  6. The System SOL version 2020

    Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju

    Proceedings of the 9th International Workshop on Confluence (IWC 2020)　81-81　2020年6月

  7. Polymorphic computation systems: Theory and practice of confluence with call-by-value 査読有り

    Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi

    Sci. Comput. Program.　187　102322-102322　2020年

    DOI： 10.1016/j.scico.2019.102322 　

  8. Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation 査読有り

    Kentaro Kikuchi, Takahito Aoto, Isao Sasano

    Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019, Porto, Portugal, October 7-9, 2019.　13:1-13:14　2019年

    出版者・発行元： ACM

    DOI： 10.1145/3354166.3354178 　

  9. The System SOL version 2018

    Makoto Hamana, Kentaro Kikuchi

    Proceedings of the 7th International Workshop on Confluence (IWC 2018)　70-70　2018年7月

  10. ACPH: System Description for CoCo 2017

    Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 6th International Workshop on Confluence (IWC 2017)　70-70　2017年9月8日

  11. Confluence by Strong Commutation with Disjoint Parallel Reduction 査読有り

    Kentaro Kikuchi

    Participant's Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)　2017年9月8日

  12. Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems 査読有り

    Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)　LNAI 10483　115-131　2017年

    出版者・発行元： Springer Verlag

    DOI： 10.1007/978-3-319-66167-4_7 　

    ISSN：1611-3349 0302-9743

  13. ACPH: System Description for CoCo 2016

    Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)　76-76　2016年9月8日

  14. Nrbox: System Description for CoCo 2016

    Takahito Aoto, Kentaro Kikuchi

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)　87-87　2016年9月8日

  15. A Rule-Based Procedure for Equivariant Nominal Unification 査読有り

    Takahito Aoto, Kentaro Kikuchi

    Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016)　2016年6月25日

  16. Critical Pair Analysis in Nominal Rewriting 査読有り

    Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 7th International Symposium on Symbolic Computation in Software Science (SCSS 2016)　EPiC 39　156-168　2016年3月27日

    出版者・発行元：

    DOI： 10.29007/7q54 　

  17. Nominal Confluence Tool 査読有り

    Takahito Aoto, Kentaro Kikuchi

    Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)　LNAI 9706　173-182　2016年

    出版者・発行元： Springer Verlag

    DOI： 10.1007/978-3-319-40229-1_12 　

    ISSN：1611-3349 0302-9743

  18. Correctness of Context-Moving Transformations for Term Rewriting Systems 査読有り

    Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015)　LNCS 9527　331-345　2015年12月

    DOI： 10.1007/978-3-319-27436-2_20 　

    ISSN：0302-9743

  19. ACPH: System Description

    Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 4th International Workshop on Confluence (IWC 2015)　39-39　2015年8月2日

  20. NoCo: System Description for CoCo 2015

    Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto

    Proceedings of the 4th International Workshop on Confluence (IWC 2015)　48-48　2015年8月2日

  21. Context-Moving Transformation for Term Rewriting Systems (Extended Abstract) 査読有り

    Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Participant's Proceedings of the 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)　3-7　2015年7月2日

  22. Confluence of Orthogonal Nominal Rewriting Systems Revisited 査読有り

    Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015)　LIPIcs 36　301-317　2015年6月

    出版者・発行元： Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

    DOI： 10.4230/LIPIcs.RTA.2015.301 　

    ISSN：1868-8969

  23. 項書き換えシステムの変換を利用した帰納的定理自動証明 査読有り

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    コンピュータソフトウェア　32　(1)　179-193　2015年2月

    DOI： 10.11309/jssst.32.1_179 　

  24. Uniform Proofs of Normalisation and Approximation for Intersection Types 査読有り

    Kentaro Kikuchi

    Proceedings of the 7th Workshop on Intersection Types and Related Systems (ITRS 2014)　EPTCS 177　10-23　2015年2月

    DOI： 10.4204/EPTCS.177.2 　

  25. Automated inductive theorem proving using transformations of term rewriting systems

    Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Computer Software　32　(1)　179-193　2015年

    出版者・発行元： Japan Society for Software Science and Technology

    ISSN：0289-6540

  26. A Translation of Intersection and Union Types for the λμ-Calculus (short paper) 査読有り

    Kentaro Kikuchi, Takafumi Sakurai

    Proceedings of the 5th International Workshop on Classical Logic and Computation (CL&C 2014)　2014年

  27. A Translation of Intersection and Union Types for the λμ-Calculus 査読有り

    Kentaro Kikuchi, Takafumi Sakurai

    Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014)　LNCS 8858　120-139　2014年

    出版者・発行元：

    DOI： 10.1007/978-3-319-12736-1_7 　

    ISSN：0302-9743

    eISSN：1611-3349

  28. Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended λ-Calculus 査読有り

    Kentaro Kikuchi

    Proceedings of the 22nd Annual Conference of the European Association for Computer Science Logic (CSL 2013)　LIPIcs 23　395-414　2013年

    出版者・発行元： Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

    DOI： 10.4230/LIPIcs.CSL.2013.395 　

    ISSN：1868-8969

  29. On General Methods for Proving Reduction Properties of Typed Lambda Terms

    Kentaro Kikuchi

    証明論と論理・計算の構造，京都大学数理解析研究所講究録　1635　33-50　2009年

  30. Strong Normalisation of Cut-Elimination that Simulates β-Reduction 査読有り

    Kentaro Kikuchi, Stéphane Lengrand

    Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2008)　LNCS 4962　380-394　2008年

    DOI： 10.1007/978-3-540-78499-9_27 　

    ISSN：0302-9743 1611-3349

  31. Call-by-Name Reduction and Cut-Elimination in Classical Logic 査読有り

    Kentaro Kikuchi

    Annals of Pure and Applied Logic　153　(1-3)　38-65　2008年

    DOI： 10.1016/j.apal.2008.01.002 　

    ISSN：0168-0072

  32. A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic 査読有り

    Ryo Ishigaki, Kentaro Kikuchi

    Logic Journal of the Interest Group in Pure and Applied Logics　15　(2)　149-164　2007年

    DOI： 10.1093/jigpal/jzm004 　

    ISSN：1367-0751

  33. Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi 査読有り

    Kentaro Kikuchi

    Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007)　LNCS 4533　257-272　2007年

    DOI： 10.1007/978-3-540-73449-9_20 　

    ISSN：0302-9743

  34. Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus 査読有り

    Kentaro Kikuchi

    Proceedings of the 3rd Conference on Computability in Europe (CiE 2007)　LNCS 4497　398-407　2007年

    DOI： 10.1007/978-3-540-73001-9_41 　

    ISSN：0302-9743 1611-3349

  35. Tree-Sequent Methods for Subintuitionistic Predicate Logics 査読有り

    Ryo Ishigaki, Kentaro Kikuchi

    Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007)　LNAI 4548　149-164　2007年

    DOI： 10.1007/978-3-540-73099-6_13 　

  36. Call-by-Name Reduction and Cut-Elimination in Classical Logic 査読有り

    Kentaro Kikuchi

    Proceedings of the 1st International Workshop on Classical Logic and Computation (CL&C 2006)　2006年

  37. On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus 査読有り

    Kentaro Kikuchi

    Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006)　LNAI 4246　120-134　2006年

    DOI： 10.1007/11916277_9 　

    ISSN：0302-9743

  38. A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus 査読有り

    Kentaro Kikuchi

    Proceedings of the 7th International Symposium on Functional and Logic Programming (FLOPS 2004)　LNCS 2998　244-259　2004年

    DOI： 10.1007/978-3-540-24754-8_18 　

    ISSN：0302-9743

  39. A Cut-Free Gentzen Formulation of Basic Propositional Calculus 査読有り

    Kentaro Kikuchi, Katsumi Sasaki

    Journal of Logic, Language and Information　12　(2)　213-225　2003年

    DOI： 10.1023/A:1022363219134 　

  40. Dual-Context Sequent Calculus and Strict Implication 査読有り

    Kentaro Kikuchi

    Mathematical Logic Quarterly　48　(1)　87-92　2002年

    DOI： 10.1002/1521-3870(200201)48:1<87::AID-MALQ87>3.0.CO;2-N 　

    ISSN：0942-5616

  41. Sequent Calculi for Visser's Propositional Logics 査読有り

    Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi

    Notre Dame Journal of Formal Logic　42　(1)　1-22　2001年

    DOI： 10.1305/ndjfl/1054301352 　

    ISSN：1939-0726 0029-4527

  42. Relationships between Basic Propositional Calculus and Substructural Logics 査読有り

    Kentaro Kikuchi

    Bulletin of the Section of Logic　30　(1)　15-20　2001年

  43. Cut-Free Sequent Calculi for Visser's Propositional Logics

    Kentaro Kikuchi

    Research Report IS-RR-99-0030F, Japan Advanced Institute of Science and Technology　1999年

︎全件表示 ︎最初の5件までを表示

講演・口頭発表等 40

  1. 定理証明支援系による動的型をもつプログラミング言語の検証基盤の実装

    齋藤 佑貴, 中野 圭介, 浅田 和之, 菊池 健太郎

    第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026)　2026年3月11日

  2. IsoLang: a User-Friendly Reversible Programming Language with Inductive Types

    Kosuke Onodera, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi

    第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026)　2026年3月9日

  3. Elpiを利用したインタプリタ生成コマンドの実装

    齋藤 佑貴, 中野 圭介, 浅田 和之, 菊池 健太郎

    第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025)　2025年3月5日

  4. 定理証明支援系におけるプロパティベーステストのための網羅的関数生成

    野木 知優, 中野 圭介, 浅田 和之, 菊池 健太郎, 佐藤 龍之介

    第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025)　2025年3月5日

  5. 機械学習におけるアーキテクチャ構成とその学習手法の圏論的構造化 招待有り

    中村 卓武, 浅田 和之, 菊池 健太郎, 中野 圭介

    日本ソフトウェア科学会第41回大会　2024年9月10日

  6. 項書き換え系における局所十分完全性判定手続きの順序ソートによる拡張とその実装

    齋藤 佑貴, 菊池 健太郎, 中野 圭介, 浅田 和之

    第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)　2024年3月5日

  7. トップダウン型自動微分をもつ圏における訓練データ逆伝播法とそれによる勾配に基づく学習

    中村 卓武, 浅田 和之, 菊池 健太郎, 中野 圭介

    第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)　2024年3月5日

  8. 定理証明支援系によるJavaScriptプログラムの検証基盤の開発にむけて

    上西 真由, 中野 圭介, 浅田 和之, 菊池 健太郎, 野木 知優

    第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)　2024年3月5日

  9. 型変換による異なる定理証明支援系間の証明の再利用

    菅野 直孝, 中野 圭介, 浅田 和之, 菊池 健太郎

    第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)　2024年3月5日

  10. Characterizations of Partial Well-Behaved Lenses

    Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi

    第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)　2024年3月5日

  11. 異なる定理証明支援系間の証明の再利用に向けた帰納型の変換

    菅野 直孝, 中野 圭介, 浅田 和之, 菊池 健太郎

    日本ソフトウェア科学会第40回大会　2023年9月13日

  12. 定理証明支援系Coqによる言語の非正規性の証明

    野木 知優, 中野 圭介, 浅田 和之, 菊池 健太郎

    第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)　2023年3月6日

  13. 定理証明支援系間の証明の相互変換

    菅野 直孝, 中野 圭介, 浅田 和之, 菊池 健太郎

    第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)　2023年3月6日

  14. Σ半環上の加群の係数制限と係数拡大による新たな線形論理モデルの構成

    伊藤 耀, 中野 圭介, 浅田 和之, 菊池 健太郎

    第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)　2023年3月6日

  15. アトム変数を用いた名目単一化の実装

    山上隼司, 菊池健太郎, 上野雄大, 大堀淳

    日本ソフトウェア科学会第38回大会　2021年9月2日

  16. 名目書き換えにおける強可換性を用いた合流性証明

    菊池健太郎

    日本ソフトウェア科学会第37回大会　2020年9月10日

  17. 項書き換えシステムにおける局所十分完全性の証明法

    白石智輝, 青戸等人, 菊池健太郎

    第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020)　2020年3月2日

  18. 無限のデータを含む等式に対する帰納的定理証明

    菊池健太郎, 篠埜功

    日本ソフトウェア科学会第35回大会　2018年8月29日

  19. 完備化手続きにおける関数記号導入の戦略

    伊藤佑太, 菊池健太郎, 外山芳人

    平成28年度 電気関係学会東北支部連合大会　2016年8月30日

  20. 項書き換えシステムの基底合流性の自動検証

    神野祐磨, 菊池健太郎, 青戸等人, 外山芳人

    第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)　2016年3月7日

  21. 高階書き換えシステムの合流性自動検証ツール

    小野沢倖太, 菊池健太郎, 青戸等人, 外山芳人

    第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)　2016年3月7日

  22. 文脈移動法によるプログラム変換の正当性について

    菊池健太郎, 青戸等人, 外山芳人

    日本ソフトウェア科学会第32回大会　2015年9月8日

  23. 高階書き換えシステムの合流性

    小野沢倖太, 菊池健太郎, 青戸等人, 外山芳人

    平成27年度 電気関係学会東北支部連合大会　2015年8月27日

  24. 項書き換えシステムの基底合流性の自動検証

    神野祐磨, 菊池健太郎, 青戸等人, 外山芳人

    平成27年度 電気関係学会東北支部連合大会　2015年8月27日

  25. 名目書き換えシステムの合流性について

    鈴木貴樹, 菊池健太郎, 青戸等人, 外山芳人

    第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)　2014年3月5日

  26. 帰納的定理自動証明のための項書き換えシステム自動変換

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)　2014年3月5日

  27. Non-deterministic CPS-translation for lambda-mu calculus

    菊池健太郎

    第30回記号論理と情報科学研究集会 (SLACS 2013)　2013年9月24日

  28. 自動検証のためのプログラム変換法

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    日本ソフトウェア科学会第30回大会　2013年9月10日

  29. 束縛変数を考慮した名目書き換えシステムの実現法

    鈴木貴樹, 菊池健太郎, 青戸等人, 外山芳人

    第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013)　2013年3月4日

  30. 文脈移動法に基づく項書き換えシステムの自動変換

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013)　2013年3月4日

  31. 等式付き項書き換えシステムの完備化

    内田和真, 菊池健太郎, 青戸等人, 外山芳人

    平成24年度 電気関係学会東北支部連合大会　2012年8月30日

  32. 木オートマトンをもちいた交差不能性判定

    四方駿作, 菊池健太郎, 青戸等人, 外山芳人

    平成24年度 電気関係学会東北支部連合大会　2012年8月30日

  33. 部分直観主義述語論理の公理化について

    菊池健太郎

    証明論研究集会 (Proof Theory 2009)　2010年2月21日

  34. On General Methods for Proving Reduction Properties of Typed Lambda Terms

    菊池健太郎

    証明論研究集会 (Proof Theory 2008)　2008年9月8日

  35. ベータ簡約を模倣するカット除去手続き

    菊池健太郎

    第24回記号論理と情報科学研究集会 (SLACS 2007)　2007年9月18日

  36. On General Methods for Proving Properties of Typed Lambda Terms 国際会議

    Kentaro Kikuchi

    Austria-Japan Summer Workshop on Term Rewriting　2005年8月8日

  37. A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus

    菊池健太郎

    第6回プログラミングおよびプログラミング言語ワークショップ (PPL 2004)　2004年3月11日

  38. 明示的代入計算とカット除去の強正規化性について

    菊池健太郎

    第19回記号論理と情報科学研究集会 (SLACS 2002)　2002年9月18日

  39. Dual-Context Sequent Calculus and Strict Implication

    菊池健太郎

    証明論研究集会 (Proof Theory 2001)　2001年12月17日

  40. Cut-free Sequent Calculi for Visser's Propositional Logics

    菊池健太郎

    第33回数理論理学研究集会 (MLG 2000)　2000年1月10日

︎全件表示 ︎最初の5件までを表示