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

[koba]

皆様、

東京大学の小林と申します．
以下の特任研究員の募集の件、締切りが過ぎましたが10月30日まで待ちたいと思います。
もしご興味のある方がいらっしゃいましたら（正式な応募でなくても）まずご一報ください。
学振PD等に応募中の方もその旨お伝えいただければ結構です
年度単位の更新はありますが最長4年ですのでポスドクとしては比較的安定したポジションだと
思います。

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


From: koba <koba at kb.is.s.u-tokyo.ac.jp>
Subject: [jssst-ppl] 特任研究員の募集
Date: Tue, 18 Aug 2015 14:13:25 +0900 (JST)

> 
> ＃複数受け取られましたらご容赦ください．
> 
>  東京大学の小林と申します．
> 
> 
>   当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）と
>  そのプログラム検証などへの応用をテーマとした研究を精力的に進めており，
>  プロジェクトに携わる特任研究員若干名を探しております．
> 
>   身近にご興味のある方がいらっしゃいましたら，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)
> _______________________________________________
> jssst-ppl mailing list
> jssst-ppl at fos.kuis.kyoto-u.ac.jp
> http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/jssst-ppl