＃複数受け取られましたらご容赦ください．
東京大学の小林と申します．
当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）と そのプログラム検証などへの応用をテーマとした研究を精力的に進めており， プロジェクトに携わる特任研究員を探しております．
身近にご興味のある方がいらっしゃいましたら，10月20日までに小林 (koba@is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。 その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるか または郵送でお送りください。 （後日、さらに詳細な資料をお願いする可能性があります）．
募集の条件は概ね以下のとおりです。
================ 着任時期：2018年4月（数ヵ月の前後は応相談）
任期：年度単位の更新で、業績により最長2020年3月まで延長可能
給与：月額38～45万円 （大学の規定および本人の実績による．細かい条件は応相談.）
研究テーマ： 高階モデル検査（高階再帰スキームのモデル検査）および、 そのプログラム検証やデータ圧縮、知識発見などへの応用。
高階モデル検査については，プロジェクトのページ http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/ および下の参考文献をご覧ください。
本プロジェクトは科学研究費補助金 基盤研究(S)：
課題名： 高階モデル検査の深化と発展 研究代表者： 小林直樹（東京大学） 研究分担者： 五十嵐 淳（京都大学）、篠原 歩（東北大学）
の支援をいただいており、その補助金で研究員を雇用する予定です。
条件： - 着任時に博士号を取得していること
- 理論計算機科学全般に明るいこと．
- 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、 ２つ以上のトピックに詳しいこと
モデル検査（特にソフトウェアモデル検査） 型システム プログラム意味論 プログラム解析・検証・変換 オートマトンと形式言語理論 自動定理証明 計算量理論 (可逆)データ圧縮技術 自然言語処理 ゲノムデータ解析
問い合わせ先： 小林直樹 東京大学大学院情報理工学系研究科コンピュータ科学専攻 〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4114 email: koba@is.s.u-tokyo.ac.jp
参考文献の抜粋 ------------- 高階モデル検査の概要：
Naoki Kobayashi, "Model Checking Higher-Order Programs", Journal of the ACM, 60(3), 2013.
Naoki Kobayashi, "Higher-Order Model Checking: From Theory to Practice", Invited paper in Proceedings of LICS 2011. (A very brief survery of the field)
高階モデル検査/高階言語の理論： Naoki Kobayashi, Etienne Lozes, Florian Bruse, "On the relationship between higher-order recursion schemes and higher-order fixpoint logic", POPL 2017, pp.246-259, 2017
Kazuyuki Asada, Naoki Kobayashi, "Pumping Lemma for Higher-order Languages", ICALP 2017, 97:1-97:14, 2017.
Ryoma Sinya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada, "Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence", FoSSaCS 2017, pp.53-68
プログラム検証への応用:
Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno, "Predicate Abstraction and CEGAR for Higher-Order Model Checking", Proceedings of PLDI 2011, pp.222-233, 2011.
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, "Temporal verification of higher-order functional programs", POPL 2016, pp.57-68
データ圧縮への応用: Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi, "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2(1), pp.39-84, 2012.
＃複数受け取られましたらご容赦ください．
東京大学の小林と申します．
当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）と そのプログラム検証などへの応用をテーマとした研究を精力的に進めており， プロジェクトに携わる特任研究員を探しております．
身近にご興味のある方がいらっしゃいましたら，小林(koba@is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。 その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるか または郵送でお送りください。 （後日、さらに詳細な資料をお願いする可能性があります）．
募集の条件は概ね以下のとおりです。 応募締切は設定しておりません。先着順に適正を審査して選考します。
================ 着任時期：2018年8月以降のなるべく早い時期
任期：2020年3月まで
給与：月額40～50万円 （大学の規定および本人の実績による．細かい条件は応相談.）
研究テーマ： 高階モデル検査（高階再帰スキームのモデル検査）および、 そのプログラム検証やデータ圧縮、知識発見などへの応用。
高階モデル検査については，プロジェクトのページ http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/ および下の参考文献をご覧ください。
本プロジェクトは科学研究費補助金 基盤研究(S)：
課題名： 高階モデル検査の深化と発展 研究代表者： 小林直樹（東京大学） 研究分担者： 五十嵐 淳（京都大学）、篠原 歩（東北大学）
の支援をいただいており、その補助金で研究員を雇用する予定です。
条件： - 着任時に博士号を取得していること
- 理論計算機科学全般に明るいこと．
- 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、 ２つ以上のトピックに詳しいこと
モデル検査（特にソフトウェアモデル検査） 型システム プログラム意味論 プログラム解析・検証・変換 オートマトンと形式言語理論 自動定理証明 計算量理論 (可逆)データ圧縮技術 自然言語処理 ゲノムデータ解析
問い合わせ先： 小林直樹 東京大学大学院情報理工学系研究科コンピュータ科学専攻 〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4114 email: koba@is.s.u-tokyo.ac.jp
参考文献の抜粋 ------------- 高階モデル検査の概要：
Naoki Kobayashi, "Model Checking Higher-Order Programs", Journal of the ACM, 60(3), 2013.
Naoki Kobayashi, "Higher-Order Model Checking: From Theory to Practice", Invited paper in Proceedings of LICS 2011. (A very brief survery of the field)
高階モデル検査/高階言語の理論： Naoki Kobayashi, Etienne Lozes, Florian Bruse, "On the relationship between higher-order recursion schemes and higher-order fixpoint logic", POPL 2017, pp.246-259, 2017
Kazuyuki Asada, Naoki Kobayashi, "Pumping Lemma for Higher-order Languages", ICALP 2017, 97:1-97:14, 2017.
Ryoma Sinya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada, "Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence", FoSSaCS 2017, pp.53-68
プログラム検証への応用:
Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno, "Predicate Abstraction and CEGAR for Higher-Order Model Checking", Proceedings of PLDI 2011, pp.222-233, 2011.
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, "Temporal verification of higher-order functional programs", POPL 2016, pp.57-68
データ圧縮への応用: Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi, "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2(1), pp.39-84, 2012.
logic-ml@fos.kuis.kyoto-u.ac.jp
-
koba＠kb.is.s.u-tokyo.ac.jp