[logic-ml] 特任研究員の募集

[koba]

＃複数受け取られましたらご容赦ください．

 東京大学の小林と申します．


  当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）と
 そのプログラム検証などへの応用をテーマとした研究を精力的に進めており，
 プロジェクトに携わる特任研究員若干名を探しております．

  身近にご興味のある方がいらっしゃいましたら，10月15日までに小林
  (koba at is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。
 その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるか
 または郵送でお送りください。
  （後日、さらに詳細な資料をお願いする可能性があります）．

  募集の条件は概ね以下のとおりです。

 ================
  着任時期：2016年4月（数ヵ月の前後は応相談）

  任期：年度単位の更新で、業績により最長2020年3月まで延長可能

  給与：月額35～45万円
　　（大学の規定および本人の実績による．細かい条件は応相談.）

  研究テーマ：
    高階モデル検査（高階再帰スキームのモデル検査）および、
    そのプログラム検証やデータ圧縮、知識発見などへの応用。

    高階モデル検査については，プロジェクトのページ
　　　http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/
    および下の参考文献をご覧ください。

　　本プロジェクトは科学研究費補助金 基盤研究(S)：

　　　 課題名： 高階モデル検査の深化と発展
　　　 研究代表者： 小林直樹（東京大学）
　　　 研究分担者： 五十嵐 淳（京都大学）、篠原 歩（東北大学）

　　の支援をいただいており、その補助金で研究員を雇用する予定です。

  条件：
    - 着任時に博士号を取得していること

    - 理論計算機科学全般に明るいこと．

    - 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、
　　　２つ以上のトピックに詳しいこと

         モデル検査（特にソフトウェアモデル検査）
         型システム
         プログラム意味論
         プログラム解析・検証・変換
         オートマトンと形式言語理論
         自動定理証明
 　　　　　計算量理論
         (可逆)データ圧縮技術
         自然言語処理
         ゲノムデータ解析

  問い合わせ先：
　　小林直樹
　　東京大学大学院情報理工学系研究科コンピュータ科学専攻
　　〒113-0033 東京都文京区本郷7-3-1
　　Phone, Fax: 03-5841-4124
　　email: koba at is.s.u-tokyo.ac.jp



参考文献：

Naoki Kobayashi, "Model Checking Higher-Order Programs", 
Journal of the ACM, 60(3), 2013.

Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno,
 "Predicate Abstraction and CEGAR for Higher-Order Model Checking",
 Proceedings of PLDI 2011, pp.222-233, 2011.

Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi,
 "Functional Programs as Compressed Data", 
 Higher-Order and Symbolic Computation, 2(1), pp.39-84, 2012.

Naoki Kobayashi,
 "Higher-Order Model Checking: From Theory to Practice",
 Invited paper in Proceedings of LICS 2011.
 (A very brief survery of the field)