計算論理学研究室（JAIST）

連絡先

• 教員名：高木翼（准教授）
• 所属：北陸先端科学技術大学院大学 (JAIST)、情報科学系、コンピューティング科学領域
• メールアドレス：
• 部屋：I-54b（情報科学系研究棟5階）
• 見学/入学希望の場合はまずメールで問い合わせてください（オンライン面談も可能）

研究分野

当研究室が取り組んでいる研究分野は理論計算機科学です。現在の高度IT社会においては、誰もがスマートフォンやパソコンといった広義の「計算機」を活用して豊かな生活を送っています。当研究室では、「計算機」を単なる道具として使うことに留まらず、その仕組みを理論的に再定式化したり、新たに考案する研究を行っています。

具体的には、数理論理学という数学の一分野を応用して、プログラミングの機能、あるいはソフトウェアや通信プロトコルの仕様などを科学的に探究しています。さらに、その成果によってアルゴリズムやプログラムの正しさを数学的に担保する形式検証という技術を発展させることで、高信頼ソフトウェアの実現を目指しています。

キーワード：形式仕様/検証、多ソート等式論理、様相論理、動的論理（ホーア論理）、時相論理（モデル検査）、量子論理、普遍代数、状態遷移系、並行計算、量子計算、量子プログラム/プロトコル

研究の立場

• 基本的には定義・定理・証明の流れで議論を展開する
• ただし、モチベーションは数学ではなく計算機科学にある
• 理論の有効性を実証するためにプログラミングによる実装も行うことがある

研究紹介

• 研究紹介（一般向け）
• 研究紹介（専門家向け）
• 研究業績 (researchmap)
• 解説記事（計算機科学と様相論理の関係）
• プレスリリース(JAIST)・新聞記事(日本経済新聞)（並行量子通信プロトコルの形式検証）

学生指導方針

• 各学生のバックグラウンド（学部で学んだ内容や得意・不得意など）やモチベーション（何を研究したいか、何を習得したいかなど）を最大限考慮します
• 理論系のバックグラウンドをもたない学生には数学の初歩から指導します
• 開かれた研究室を目指して、自主・自律・自由の精神を重んじています

研究者は、これまで誰も提案したことのない新たなプログラミングや仕様記述の機能や仕組みの開発や定式化などを行います。当研究室では、数学の基礎知識を着実に身に着けたうえで、（単なる理論のための理論ではなく）応用や実装を志向した新理論の確立と洗練に取り組めます。百年後の社会にも影響を与えることができるような洗練された理論の構築が目標です。

ある一定水準を超える技術者には高度な専門知識が求められます。具体的には、単にプログラミングや仕様記述が行えるだけでなく、その動作原理や機能の数学を用いた厳密な理解が必要です。当研究室では、関数型プログラミング言語を用いた命令型プログラミング言語のインタプリタやコンパイラの設計、型理論と普遍代数に基づく形式仕様の記述、通信プロトコルや分散システムの解析（モデル検査）などに取り組めます。

学生生活について

• 週に1回の進捗報告会以外に学生が参加必須のイベントはありません
• 好きな時間に研究室に来て、好きな時間に帰ってください
• 必要があれば、基礎知識を学ぶ勉強会や研究室合宿を開催します（参加自由）
• 就活や帰省等で忙しい時期に研究活動を強制することは一切ありません
• じっくり学びたい学生には、長期履修制度（二年分の授業料で三年間在籍可能）もあります
• 予算の都合がつけばLA (Laboratory Assistant)やRA (Research Assistant)として謝金を払うことも可能
• 博士課程の学生は希望者全員をUA (University Assistant)として採用し謝金を払います
• 博士課程の学生は日本学術振興会特別研究員もしくはJAIST次世代特別研究員に選ばれれば、生活費・研究費の支援の下で研究に専念可能（奨学金情報も参照）

教科書

当研究室の研究内容と関連のある教科書をいくつか挙げます。基本的には、配属後はこれらの教科書（のうち数冊）を読むことになります。いずれの教科書も、高木研究室またはJAIST図書館に配架済みです。

大学教養程度の数学を履修していない場合は読むことを推奨します。

• 集合・位相入門（松坂和夫、集合の部分のみ必要）
• 代数系入門（松坂和夫）

• Theorem Proving and Algebra (Joseph Goguen)
• Specification of Abstract Data Types (Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf)
• Foundations of Algebraic Specification and Formal Software Development (Donald Sannella, Andrzej Tarlecki)

• モデルの記述と検証のためのプログラミング入門: CafeOBJによる仕様検証（二木 厚吉）
• Algebraic Semantics of Imperative Programs (Joseph Goguen, Grant Malcolm)
• Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude (Peter Csaba Ölveczky)

構成員

• 高木 翼（准教授）
• Yang Song（研究員）
• 小林 脩亮（M1）
• 中村 太陽（M1）
• 名越 龍一（M1）
• 山口 快（M1）

当研究室では、研究員を公募しています．