菊池 健太郎

〒980-8577 宮城県 仙台市 青葉区 片平 2-1-1
東北大学 電気通信研究所 コンピューティング情報理論研究室 助教 (動画

研究業績一覧(説明

査読付き国際会議・学術雑誌論文(リンク等は英語のページを参照)

[1] Nominal Confluence Tool
   Takahito Aoto, Kentaro Kikuchi
   Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016) LNAI 9706 pp.173-182 2016年
[2] 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 Series in Computing 39 pp.156-168 2016年
[3] 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 pp.331-345 2015年
[4] 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 pp.301-317 2015年
[5] 項書き換えシステムの変換を利用した帰納的定理自動証明
   佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
   コンピュータソフトウェア 32(1) pp.179-193 2015年
[6] 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 pp.10-23 2015年
[7] 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 pp.120-139 2014年
[8] 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 pp.395-414 2013年
[9] Call-by-Name Reduction and Cut-Elimination in Classical Logic
   Kentaro Kikuchi
   Annals of Pure and Applied Logic 153(1-3) pp.38-65 2008年
[10] 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 pp.380-394 2008年
[11] 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 pp.149-164 2007年
[12] 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 pp.257-272 2007年
[13] 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 pp.398-407 2007年
[14] 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) pp.149-164 2007年
[15] 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 pp.120-134 2006年
[16] 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 pp.244-259 2004年
[17] A Cut-Free Gentzen Formulation of Basic Propositional Calculus
   Kentaro Kikuchi, Katsumi Sasaki
   Journal of Logic, Language and Information 12(2) pp.213-225 2003年
[18] Dual-Context Sequent Calculus and Strict Implication
   Kentaro Kikuchi
   Mathematical Logic Quarterly 48(1) pp.87-92 2002年
[19] Sequent Calculi for Visser's Propositional Logics
   Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi
   Notre Dame Journal of Formal Logic 42(1) pp.1-22 2001年
[20] Relationships between Basic Propositional Calculus and Substructural Logics
   Kentaro Kikuchi
   Bulletin of the Section of Logic 30(1) pp.15-20 2001年

査読付きワークショップ論文

[21] A Rule-Based Procedure for Equivariant Nominal Unification
   Takahito Aoto, Kentaro Kikuchi
   Participant's Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016) 2016年
[22] 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) 2015年
[23] 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年
[24] 名目書き換えシステムの合流性について
   鈴木貴樹, 菊池健太郎, 青戸等人, 外山芳人
   第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014) 論文集 2014年
[25] 帰納的定理自動証明のための項書き換えシステム自動変換
   佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
   第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014) 論文集 2014年
[26] 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年

その他の研究論文

[27] On General Methods for Proving Reduction Properties of Typed Lambda Terms
   Kentaro Kikuchi
   証明論と論理・計算の構造, 京都大学数理解析研究所講究録 1635 pp.33-50 2009年
[28] Gentzen Style Sequent Calculi for Some Subsystems of Intuitionistic Logic
   Kentaro Kikuchi
   PhD thesis, Japan Advanced Institute of Science and Technology 2002年
[29] 証明論におけるメタ定理のCafeOBJによる検証
   菊池健太郎
   博士後期課程副テーマ論文, 北陸先端科学技術大学院大学 2001年
[30] 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年
[31] A Logic with Implication Expressing Temporality
   Kentaro Kikuchi
   MSc thesis, Japan Advanced Institute of Science and Technology 1999年
[32] CafeOBJによるプログラム言語の意味定義
   菊池健太郎
   博士前期課程副テーマ論文, 北陸先端科学技術大学院大学 1998年
[33] 時間論理の形式的体系に関する研究
   菊池健太郎
   卒業論文, 東京工業大学工学部情報工学科 1997年

競争的資金等の研究課題

科学研究費補助金(代表のみ)

基盤研究 (C) 2016年4月--2019年3月
「文脈移動変換と高階書き換え理論に基づくプログラム検証法の研究」(代表)
総額 3,510,000円

若手研究 (B) 2005年4月--2007年3月
「シーケント計算に基づく型システムの研究」(代表)
総額 1,000,000円

特別研究員奨励費 2002年4月--2005年3月
「非古典論理によるソフトウェア記述へのアプローチ」(代表)
総額 3,400,000円

担当経験のある科目

(学部教育)
プログラミング演習B 2006, 2009, 2012--2016年度(シラバス
電気・通信・電子・情報工学実験A 2005, 2007--2008年度
電気・通信・電子・情報工学実験B 2010--2011年度
電気・通信・電子・情報工学実験D 2006--2015年度(説明
電気・通信・電子・情報工学セミナー 2005年度

(全学教育)
基礎ゼミ「認識・記憶・処理・伝達」 2005年度