高木翼（准教授）
連絡先
- 所属：北陸先端科学技術大学院大学 (JAIST)、情報科学系、コンピューティング科学領域
- メールアドレス：
- 部屋：I-54b（情報科学系研究棟5階）
- オフィスアワー：毎週月曜日15時から16時（この時間帯は事前連絡なしで訪問可）
- 入学/見学希望の場合はまずメールで問い合わせてください
研究分野
当研究室が取り組んでいる研究分野は理論計算機科学です。現在の高度IT社会においては、誰もがスマートフォンやパソコンといった広義の「計算機」を活用して豊かな生活を送っています。当研究室では、「計算機」を単なる道具として使うことに留まらず、その仕組みを理論的に再定式化したり、新たに考案する研究を行っています。
具体的には、数理論理学という数学の一分野を応用して、プログラミングの機能、あるいはソフトウェアや通信プロトコルの仕様などを科学的に探究しています。さらに、その成果によってアルゴリズムやプログラムの正しさを数学的に担保する形式検証という技術を発展させることで、高信頼ソフトウェアの実現を目指しています。
キーワード
形式仕様/検証、多ソート等式論理、様相論理、動的論理（ホーア論理）、時相論理（モデル検査）、量子論理、普遍代数、状態遷移系、並行計算、量子計算、量子プログラム/プロトコル
研究の立場
- 基本的には定義・定理・証明の流れで議論を展開
- ただし、モチベーションは数学ではなく計算機科学にあります
- 最終目標は理論の確立・洗練ですが、その有効性を実証するためにプログラミングによる実装も行うことがあります
学生指導方針
- 学生の自主性を尊重し、就活や帰省等で忙しい時期に研究活動を強制することは一切ありません
- 各学生のバックグラウンド（学部で学んだ内容や得意・不得意など）やモチベーション（何を研究したいか、何を習得したいかなど）を最大限考慮します
- 理論系のバックグラウンドをもたない学生には数学の初歩から指導します
- 開かれた研究室を目指して、自主・自律・自由の精神を重んじています
- 週一で進捗確認のミーティングを定期的に開催
- 必要に応じて基礎知識の勉強会も開催します
- じっくり学びたい学生には、長期履修制度（二年分の授業料で三年間在籍可能）もあります
- 予算の都合がつけばLA (Laboratory Assistant)として謝金を払うことも可能
- 博士号の取得には、世界で認められる研究成果（然るべき国際会議・国際学術誌の査読を経た論文掲載）が必要
- そのために、論文・研究計画書・研究費応募書類の添削やアカデミック・ライティング（英語）の指導を行います
- 日本学術振興会特別研究員もしくはJAIST次世代特別研究員に選ばれれば、生活費・研究費の支援の下で研究に専念可能（奨学金情報も参照）
- 希望者全員を労働対価型のUA (University Assistant)として採用
- 予算の都合がつけばRA (Research Assistant)として謝金を払うことも可能
構成員
- 高木 翼（准教授）
- Yang Song（研究員）
- 小林 脩亮（M1）
- 中村 太陽（M1）
- 名越 龍一（M1）
- 山口 快（M1）
ポスドク研究員募集中
- 業務内容
- 量子計算の形式検証に関する文献調査、論文執筆、学会発表、その他研究の遂行に必要な業務
- 給与総額
- 2,992,500円から法定の雇用・労災保険料等を減じた額
- 勤務時間
- 就業時間：9:00-17:00
- 休憩時間：12:00-13:00
- 休日：土曜日、日曜日、祝日、年末年始、その他
- 応募資格
- 情報科学もしくは関連分野の博士の学位を有する方（取得見込み可）
- 契約期間
- 2025年度、試用期間あり（採用日より1ヶ月間）
- 勤務地
- 石川県 能美市旭台1-1 北陸先端科学技術大学院大学 高木研究室
- 採用人数
- 1名
- 応募方法
- 履歴書、研究業績リスト、電子メールアドレスを含む応募者本人の連絡先を記載した書類（様式自由）を高木宛に電子メールで送付（決定次第締め切り）