高木翼（准教授）
連絡先
- 北陸先端科学技術大学院大学(JAIST)、情報科学系、コンピューティング科学領域
- メールアドレス：
- 部屋：I-54b（情報科学系研究棟5階）
- 入学/見学希望者はまずメールで問い合わせてください
研究分野
理論計算機科学、特に数理論理学および形式検証
数理論理学：論理学を数学的に探究する分野であり、計算機の創成から現在の発展に至るまで大きな役割を果たしてきました
形式検証：アルゴリズム、プロトコル、システム、プログラムの正しさを数学的に証明することをいい、安心・安全なIT社会基盤の構築に役立っています
キーワード
形式仕様/検証、多ソート等式論理、様相論理、動的論理（ホーア論理）、時相論理（モデル検査）、量子論理、普遍代数、状態遷移系、量子計算、量子プログラム/プロトコル
研究の立場
- 基本的には定義・定理・証明の流れで議論を展開
- ただし、モチベーションは数学ではなく計算機科学にあります
- 最終目標は理論の確立・洗練ですが、その有効性を実証するためにプログラミングによる実装も行うことがあります
リサーチクエスチョン
- 数学はいかにして計算機の理論を基礎づけるのか？
- 計算機の記号処理とその意味の関係は？
- 計算機の計算結果は本当に信頼できるのか？
- プログラムにバグがないことを証明するには？
学生指導方針
- 学生の自主性を尊重し、就活や帰省等で忙しい時期に研究活動を強制することは一切ありません
- コアタイムも一切ありません
- 理論系のバックグラウンドをもたない学生には数学の初歩から指導します
- 開かれた研究室を目指して、自主・自律・自由の精神を重んじています
- 一年目で講義の単位を全て取り終え、二年目は研究に専念する流れが理想
- 二年目（あるいは研究が開始した段階）から週一で進捗確認のミーティングを定期的に開催
- 必要に応じて基礎知識の勉強会も開催します
- じっくり学びたい学生には、長期履修制度（二年分の授業料で三年間在籍可能）もあります
- 博士号の取得には、世界で認められる研究成果（然るべき国際会議・国際学術誌の査読を経た論文掲載）が必要
- そのために、論文・研究計画書・研究費応募書類の添削やアカデミック・ライティング（英語）の指導を行います
- 日本学術振興会特別研究員もしくはJAIST次世代特別研究員に選ばれれば、生活費・研究費の支援の下で研究に専念可能（奨学金情報も参照）
- 希望者全員を労働対価型のUA (University Assistant)として採用
- 予算の都合がつけばRA (Research Assistant)として謝金を払うことも可能
よくある質問（修士課程学生向け）
- Q1. 理論系ってなんだか難しそう。自分でもやっていけそうですか？
- A1. 重要なのは理解したいという気持ちです。それさえあれば大丈夫なように基礎から丁寧に指導します（逆に言えば、その気持ちがなければ、こちらにはどうしようもありません）。
- Q2. 具体的にはどういった数学の基礎知識が必要ですか？
- A2. 初歩的な（つまり大学教養程度の）集合論、論理学、代数学の三つです。
- Q3. どういった学生を求めていますか？
- A3. 単に計算機を道具として使用するだけでなく、計算機の仕組みを理解したい（考案したい）という動機があるとよいです。
- Q4. 文系出身者も受け入れてますか？
- A4. 大歓迎です。高木自身も文学部出身で修士からJAISTに来ました。
よくある質問（博士課程学生向け）
- Q1. 修士号は全く関係ない分野で取りました。受け入れてくれますか？
- A1. その場合は修士課程学生として入学してください。
- Q2. 論文を何本書けば博士号を取得できますか？
- A2. どこに掲載されたかが重要です。トップジャーナルなら一本で大丈夫です。
構成員
- 高木翼（准教授）