muratak

Publications, Presentations

In English

Refreed Papers

  1. Kosuke Murata, Kento Emoto: Recursion Schemes in Coq. Lin A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science, vol. 11893, pp. 202-221. Springer, Cham (2019)

In Japanese

査読付き出版論文

  1. 村田 康佑，江本 健斗．定理証明支援系Coqにおける不等式変形記法．情報処理学会論文誌プログラミング (PRO)，Vol. 11, No. 4, pp.1-12．2018年12月．

口頭発表・査読なし論文・ポスタ発表など

  1. 【口頭発表・講演論文】村田 康佑，江本 健斗．Coq における Hylomorphism を用いたプログラム運算の検証に向けて．第22回プログラミングおよびプログラミング言語ワークショップ（PPL2020）．カテゴリ1．嬉野（現地開催は中止） (2020）
    • 論文: [PDF]，スライド: [PDF]
    • 新型コロナウイルス感染症の流行のため，本研究会の現地開催は中止となりました．代わりに，発表資料（発表スライド）を PPL 2020 へ提出しました．
    • カテゴリ 3 でも同題同内容のポスタ発表を予定しておりましたが，現地開催の中止に伴い，発表を取り下げました（つまり，カテゴリ3発表用の発表資料は提出していません）．

  2. 【口頭発表・講演論文（査読なし）】村田 康佑，江本 健斗．高度な運算定理の Coq による証明とその自動化．日本ソフトウェア科学会第36回大会，東京，2019年8月．講演論文: [PDF，外部サイト]，〈学生奨励賞受賞〉

  3. 【ポスタ発表】村田 康佑，江本 健斗．Coq を用いた高度なプログラム運算定理の検証に向けて．第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)，花巻，2019年3月．

  4. 【口頭発表・講演論文(査読なし)】村田 康佑，江本 健斗．Coq における検証されたプログラム運算の拡張．日本ソフトウェア科学会第35回大会，大阪，2018年8月．講演論文: [PDF，外部サイト]，

  5. 【ポスタ発表】村田 康佑，江本 健斗．Coq における可読性の高い形式的証明に向けて．第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)，米子，2018年3月．

卒業論文・修士論文

  1. 【修士論文】定理証明支援系 Coq によるデータ型汎用なプログラム運算．九州工業大学大学院情報工学府 先端情報工学専攻 知能情報工学専門分野，修士論文．（2020年1月提出） 論文本体：[PDF]，スライド；[PDF]
    • 本論文の第 2 章は「定理証明支援系 Coq における不等式変形記法（情報処理学会論文誌プログラミング (PRO)，Vol. 11, No. 4, pp.1-12）」に基づく内容です．
  2. 【卒業論文】定理証明支援系 Coq における二項関係を含む論理式の書き換え記法の改良に関する研究．九州工業大学 情報工学部 知能情報工学科，卒業論文．（2018年2月提出）