連絡先
- 所属：北陸先端科学技術大学院大学 (JAIST)、情報科学系、コンピューティング科学領域
- メールアドレス：
- 部屋：I-54b（情報科学系研究棟5階）
- オフィスアワー：毎週月曜日15時から16時（この時間帯は事前連絡なしで訪問可）
- 見学/入学希望の場合はまずメールで問い合わせてください（オンライン面談も可能）
研究分野
当研究室が取り組んでいる研究分野は理論計算機科学です。現在の高度IT社会においては、誰もがスマートフォンやパソコンといった広義の「計算機」を活用して豊かな生活を送っています。当研究室では、「計算機」を単なる道具として使うことに留まらず、その仕組みを理論的に再定式化したり、新たに考案する研究を行っています。
具体的には、数理論理学という数学の一分野を応用して、プログラミングの機能、あるいはソフトウェアや通信プロトコルの仕様などを科学的に探究しています。さらに、その成果によってアルゴリズムやプログラムの正しさを数学的に担保する形式検証という技術を発展させることで、高信頼ソフトウェアの実現を目指しています。
キーワード：形式仕様/検証、多ソート等式論理、様相論理、動的論理（ホーア論理）、時相論理（モデル検査）、量子論理、普遍代数、状態遷移系、並行計算、量子計算、量子プログラム/プロトコル
研究の立場
- 基本的には定義・定理・証明の流れで議論を展開する
- ただし、モチベーションは数学ではなく計算機科学にある
- 理論の有効性を実証するためにプログラミングによる実装も行うことがある
学生指導方針
- 各学生のバックグラウンド（学部で学んだ内容や得意・不得意など）やモチベーション（何を研究したいか、何を習得したいかなど）を最大限考慮します
- 理論系のバックグラウンドをもたない学生には数学の初歩から指導します
- 開かれた研究室を目指して、自主・自律・自由の精神を重んじています
研究者は、これまで誰も提案したことのない新たなプログラミングや仕様記述の機能や仕組みの開発や定式化などを行います。当研究室では、数学の基礎知識を着実に身に着けたうえで、（単なる理論のための理論ではなく）応用や実装を志向した新理論の確立と洗練に取り組めます。百年後の社会にも影響を与えることができるような洗練された理論の構築が目標です。
高度な専門知識をもつ技術者の育成ある一定水準を超える技術者には高度な専門知識が求められます。具体的には、単にプログラミングや仕様記述が行えるだけでなく、その動作原理や機能の数学を用いた厳密な理解が必要です。当研究室では、関数型プログラミング言語を用いた命令型プログラミング言語のインタプリタやコンパイラの設計、型理論と普遍代数に基づく形式仕様の記述、通信プロトコルや分散システムの解析（モデル検査）などに取り組めます。
学生生活について
- 週に1回の進捗報告会以外に学生が参加必須のイベントはありません
- 好きな時間に研究室に来て、好きな時間に帰ってください
- 必要であれば基礎知識を学ぶ勉強会や研究室合宿を開催します（参加自由）
- 就活や帰省等で忙しい時期に研究活動を強制することは一切ありません
- じっくり学びたい学生には、長期履修制度（二年分の授業料で三年間在籍可能）もあります
- 予算の都合がつけばLA (Laboratory Assistant)やRA (Research Assistant)として謝金を払うことも可能
- 博士課程の学生は希望者全員をUA (University Assistant)として採用し謝金を払います
- 博士課程の学生は日本学術振興会特別研究員もしくはJAIST次世代特別研究員に選ばれれば、生活費・研究費の支援の下で研究に専念可能（奨学金情報も参照）
構成員
- 高木 翼（准教授）
- Yang Song（研究員）
- 小林 脩亮（M1）
- 中村 太陽（M1）
- 名越 龍一（M1）
- 山口 快（M1）
ポスドク研究員募集中
- 詳しくは公募情報を参照
- 学振PDも受け入れています（事前に要相談）