理学部情報科学科

メニュー

木村大輔/講師

氏名

木村大輔

経歴

  • 2001年3月 京都大学理学部卒業
  • 2003年3月 京都大学大学院理学研究科 数学・数理解析専攻(数学)終了
  • 2007年3月 総合研究大学院大学 複合科学研究科 情報学専攻修了 博士(情報学)
  • 2007年4月 国立情報学研究所 特任研究員
  • 2009年4月 東京大学大学院情報理工学研究科 研究生
  • 2010年4月 国立情報学研究所 特任研究員
  • 2015年4月 東邦大学理学部 非常勤講師
  • 2016年4月 東邦大学理学部情報科学科 講師

専門分野

数理論理学
プログラム検証
プログラミング言語理論
型理論

主な研究課題

  • 分離論理を用いたプログラム検証
  • 関数型プログラミング言語の基礎理論
  • 古典論理に内在する計算機構

主な研究業績

<雑誌論文>
  • Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura."Spatial factorization in cyclic-proof system for separation logic".コンピュータソフトウェア, 37巻1号 125--144, 2020.
  • Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno. "Failure of Cut-Elimination in Cyclic Proofs of Separation Logic". コンピュータソフトウェア, 37巻1号, 39--52, 2020.
  • Daisuke Kimura and Makoto Tatsuta, "Call-by-value and Call-by-name Dual Calculi with Inductive and Coinductive Types". Logical Methods in Computer Science 9 (1), 2013.
  • Daisuke Kimura and Yoshihiko Kakutani, "Classical Natural Deduction for S4 Modal Logic", Special Issue of New Generation Computing, 29 (1), pp. 61-86, 2011.
  • Daisuke Kimura, "Duality between Call-by-value Reductions and Call-by-name Reductions", 情報処理学会論文誌 Vol.48 No.4, 2007.
<国内会議論文>
  • Makoto Tatsuta and Daisuke Kimura."Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic".第18回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2016), 2016.
  • Daisuke Kimura, Makoto Tatsuta. "Decidability of Entailments in Separation Logic with Arrays and Lists". 第20回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2018), 2018.
  • Daisuke Kimura, Makoto Tatsuta. "Decision Procedure for Symbolic Heaps with Arrays". 第19回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2017), 2017.
<国際会議論文>
  • Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. "Restriction on cut in cyclic proof system for symbolic heaps". In The 15th International Symposium on Functional and Logic Programming (FLOPS 2020), 2020.
  • Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. "Completeness of cyclic proofs for symbolic heaps with inductive definitions". In The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), LNCS 11893, 367--387, 2019.
  • Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura. "Cyclic Theorem Prover for Separation Logic by Magic Wand". In First Workshop on Automated Deduction for Separation Logics (ADSL) at FLoC 7 2018.
  • Daisuke Kimura and Makoto Tatsuta. "Decision Procedure for Entailment of Symbolic Heaps with Arrays". In proceedings of The 15th Asian Symposium on Programming Languages and Systems (APLAS2017), LNCS 10695, 169--189, 2017.
  • Makoto Tatsuta and Daisuke Kimura, "Separation Logic with Monadic Inductive Definitions and Implicit Existentials", In proceedings of The 13th Asian Symposium on Programming Languages and Systems (APLAS2015), LNCS 9458, 69--89, 2015.
  • Yoshihiko Kakutani and Daisuke Kimura, "Induction by Coinduction and Control Operators in Call-by-name", In proceedings of the workshop of Control Operators and their Semantics (COS2013), EPTCS 127, 101--112, 2013.
  • Daisuke Kimura and Yoshihiko Kakutani, "Classical Natural Deduction for S4 Modal Logic", In proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS2009), LNCS 5904, 243--258, 2009.
  • Daisuke Kimura and Makoto Tatsuta, "Dual Calculus with Inductive types and Coinductive types", In proceedings of Rewriting Techniques and Applications (RTA2009), LNCS 5595, 224--238, 2009.
  • Daisuke Kimura, "Call-by-value is Dual to Call-by-name, Extended", In proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS2007), LNCS 4807, 415--430, 2007.

主な担当科目

形式論理学
情報数理IB
情報数理演習IB
プログラミングA
数理科学基礎論I・II (大学院)

お問い合わせ先

東邦大学 理学部

〒274-8510
千葉県船橋市三山2-2-1
習志野学事部

【入試広報課】
TEL:047-472-0666

【学事課(教務)】
TEL:047-472-7208

【キャリアセンター(就職)】
TEL:047-472-1823

【学部長室】
TEL:047-472-7110