[logic-ml] 特任研究員の募集
koba at kb.is.s.u-tokyo.ac.jp
koba at kb.is.s.u-tokyo.ac.jp
Mon Sep 11 11:53:28 JST 2017
#複数受け取られましたらご容赦ください.
東京大学の小林と申します.
当研究室では現在,高階モデル検査(高階再帰スキームのモデル検査)と
そのプログラム検証などへの応用をテーマとした研究を精力的に進めており,
プロジェクトに携わる特任研究員を探しております.
身近にご興味のある方がいらっしゃいましたら,10月20日までに小林
(koba at is.s.u-tokyo.ac.jp) までメールでお知らせいただければ幸いです。
その際、できれば略歴および論文リスト(フォーマット自由)もメールに添えるか
または郵送でお送りください。
(後日、さらに詳細な資料をお願いする可能性があります).
募集の条件は概ね以下のとおりです。
================
着任時期:2018年4月(数ヵ月の前後は応相談)
任期:年度単位の更新で、業績により最長2020年3月まで延長可能
給与:月額38~45万円
(大学の規定および本人の実績による.細かい条件は応相談.)
研究テーマ:
高階モデル検査(高階再帰スキームのモデル検査)および、
そのプログラム検証やデータ圧縮、知識発見などへの応用。
高階モデル検査については,プロジェクトのページ
http://www-kb.is.s.u-tokyo.ac.jp/~koba/hmc/
および下の参考文献をご覧ください。
本プロジェクトは科学研究費補助金 基盤研究(S):
課題名: 高階モデル検査の深化と発展
研究代表者: 小林直樹(東京大学)
研究分担者: 五十嵐 淳(京都大学)、篠原 歩(東北大学)
の支援をいただいており、その補助金で研究員を雇用する予定です。
条件:
- 着任時に博士号を取得していること
- 理論計算機科学全般に明るいこと.
- 以下の中の1つ以上のトピックに詳しくプログラミング能力が高いか、
2つ以上のトピックに詳しいこと
モデル検査(特にソフトウェアモデル検査)
型システム
プログラム意味論
プログラム解析・検証・変換
オートマトンと形式言語理論
自動定理証明
計算量理論
(可逆)データ圧縮技術
自然言語処理
ゲノムデータ解析
問い合わせ先:
小林直樹
東京大学大学院情報理工学系研究科コンピュータ科学専攻
〒113-0033 東京都文京区本郷7-3-1
Phone: 03-5841-4124
Fax: 03-5841-4114
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,
"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.
More information about the Logic-ml
mailing list