連絡先
- 教員名：高木翼（准教授）
- 所属：北陸先端科学技術大学院大学 (JAIST)、情報科学系、コンピューティング科学研究領域
- メールアドレス：
- 部屋：I-54b（情報科学系研究棟5階）
- 当研究室にご関心のある方は、メールで直接問い合わせるか大学院進学相談会をご利用ください（オンライン面談可）
研究分野
当研究室が取り組んでいる研究分野は理論計算機科学です。現在の高度IT社会においては、誰もがスマートフォンやパソコンといった広義の「計算機」を活用して豊かな生活を送っています。当研究室では、「計算機」を単なる道具として使うことに留まらず、その仕組みを理論的に再定式化したり、新たに考案する研究を行っています。
具体的には、数理論理学という数学の一分野を応用して、プログラミングの機能、あるいはソフトウェアや通信プロトコルの仕様などを科学的に探究しています。さらに、その成果によってアルゴリズムやプログラムの正しさを数学的に担保する形式検証という技術を発展させることで、高信頼ソフトウェアの実現を目指しています。
研究紹介
学生指導方針
- 確かな研究実績（学会発表や論文出版）を積んで就活に臨みたい、あるいは博士課程に進学したい方を歓迎し、そのためのサポートを惜しみません
- 学生の積極的な査読あり国際会議での研究発表を推奨
- 当研究室の学生の実績：M2学生が国際会議SFPVV 2025に論文採択、M1学生が国際会議QCNC 2026に論文採択、M1学生が国際会議TASE 2026に論文採択、M2学生が国際会議ISSSR 2026に論文採択（学年は当時で全員別の学生）
- このように、本人の努力次第ではありますが、M1もしくはM2という入学後直ぐの時期から業績を積める環境が整っています
- 国際会議/国内学会に参加するための参加費・旅費・宿泊費は研究室が全額負担
- 当研究室の学生が国立研究開発法人科学技術振興機構（JST）の2026年度次世代研究者挑戦的研究プログラム（SPRING）に採択されました
- 当研究室の学生が独立行政法人情報処理推進機構（IPA）の2026年度未踏ターゲット事業（量子コンピューティング技術を活用したソフトウェア開発分野）に採択されました
【理論計算機科学の研究者の育成】
研究者は、これまで誰も提案したことのない新たなプログラミングや仕様記述の機能や仕組みの開発や定式化などを行います。当研究室では、数学の基礎知識を着実に身に着けたうえで、（単なる理論のための理論ではなく）応用や実装を志向した新理論の確立と洗練に取り組めます。百年後の社会にも影響を与えることができるような洗練された理論の構築が目標です。
【高度な専門知識をもつ技術者の育成】
ある一定水準を超える技術者には高度な専門知識が求められます。具体的には、単にプログラミングや仕様記述が行えるだけでなく、その動作原理や機能の数学を用いた厳密な理解が必要です。当研究室では、関数型プログラミング言語を用いた命令型プログラミング言語のインタプリタやコンパイラの設計、型理論と普遍代数に基づく形式仕様の記述、通信プロトコルや分散システムの解析（モデル検査）などに取り組めます。
学生生活について
- 当研究室は理論系の研究室なので、コアタイム等の拘束時間は一切ありません
- ただし、対面でのきめ細やかな指導を行うため、土日祝日や帰省中など以外は研究室に毎日一度は顔を出すことを推奨
- 研究室に来ると他の学生との研究の議論が発生して研究が進むという学生も多いです
- 例年、年に1回研究室合宿を開催しています（参加自由）
- 合宿中に研究の進捗を発表して議論することが参加条件
- 旅費・宿泊費は研究室が全額負担
- 予算の都合がつけばLA (Laboratory Assistant)やRA (Research Assistant)として謝金を払うことも可能
- 博士課程の学生は希望者全員をUA (University Assistant)として採用し謝金を払います
- 博士課程の学生は日本学術振興会特別研究員もしくはJAIST次世代特別研究員に選ばれれば、生活費・研究費の支援の下で研究に専念可能（奨学金情報も参照）
学修について
当研究室への配属を第一希望とする学生には、入学前後に以下の内容を学修してもらいます
- 素朴集合論：集合、関係、関数、同値類、文字列（『集合・位相入門』（松坂和夫）の第1章など）
- 代数的仕様記述の基本概念：代数的意味論に対する多ソート等式論理の完全性定理、始代数モデルであることと「ジャンクと混同がない」ことの同値性の理解（『計算モデルの基礎理論』（井田哲雄）の第7章など）
- 分散システムの基本概念：コンフィギュレーション、メッセージパッシング（同期・非同期通信やバッファ）、デッドロックとライブロック、要求仕様（到達可能性、不変性、相互排他性、応答性（活性）、弱公平性/強公平性、その他の線形時相論理式）
- 分散プロトコルの具体例：Dining Philosophers, Qlock, Alternating Bit Protocol, Peterson's algorithm, Leader Electionなど
担当講義
- 形式言語とオートマトン（I237, 1の1期）
- 形式言語とオートマトン（I237, I期 隔年開講）
- 数理論理学（I211, 2の1期）
- 数理論理学（I211, III期 隔年開講）
構成員
- 高木 翼（准教授）
- 宋 阳（研究員）
- 名越 龍一（D1）：測定型量子計算の形式検証（PPL 2025 ⁄ PRO 2025 ⁄ SFPVV 2025 ⁄ ISQR 2025 ⁄ PPL 2026）
- 佐藤 直人（M2, 東京社会人コース）：量子算術演算回路の形式検証（PPL 2026 ⁄ ISSSR 2026）
- 小林 脩亮（M2）：
- 山口 快（M2）：
- Yi Liu（M2）：量子通信ネットワークの形式検証（ISQR 2025 ⁄ QCNC 2026）
- 魯 珍赫（M2）：数学的帰納法による量子ルーティングの形式検証
- Yunhao Ni（M2）：整礎帰納法と項詳細化による形式検証
- 石橋 和愛（M1）：
- 山下 朋晃（M1）：
当研究室では、ポスドク研究員を公募しています．
修了生
【博士前期課程】
- 内田 隆貴（2026年度修了）：量子通信プロトコルの形式検証
- 中村 太陽（2025年度修了）：量子通信プロトコルの調査研究
- 名越 龍一（2025年度修了）：Improving Reliability of Measurement-based Quantum Computation by Formal Verification
【博士後期課程】