ss2025

PPLサマースクール2025
「依存型入門 - 基礎・応用・発展」
 
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第42回大会 併設企画
 
講師：叢 悠悠（東京科学大学）
講師：上村 太一（名古屋大学）
 
2025年9月2日(火) （10:30〜17:00，10:00受付開始で計画中です）
東海大学品川キャンパスおよびオンラインのハイブリッド開催
 

ニュース †

  • [2025-08-01] Webページを公開しました．
↑

参加者向け情報 †

PPLサマースクール2025は対面を中心としたハイブリッド形式で開催いたします．大会自体は対面のみの開催であることにご注意ください．

  • Zoomでのオンライン配信を行う予定です．
  • 対面・オンライン参加者用の非同期的な質疑・交流の場（SlackあるいはDiscord等）を提供予定です．
↑

概要 †

プログラミングにおいて型を意識することは不可欠で，型の効果的な利用はプログラムの可読性向上だけでなく，バグの予防や頑強なソフトウェアの効率的な開発にも繋がります．型の中でも依存型は記述性が高く，型の表現の中に通常の式を記述でき，型を第一級オブジェクトとしてプログラム中で型を引数にとる関数や型を返す関数を定義することもできます．高階型や多相型と合わせて述語論理式を型で表現できることから，カリー・ハワード同型対応を通して，型による命題記述に対して証明をプログラムの形で与える・そしてそれを型検査器で検証するという定理証明支援系の枠組みが，依存型によって支えられています．

依存型は，ソフトウェア開発においても有用です．型の記述力の高さは，プログラムの性質の記述に役立ちます．それは検証事項の明記となるだけでなく，静的検証に用いられ，プログラムの実行時の動的エラー検査の削減による実行効率向上を促進する効果もあります．またプログラミングにおいてユーザをガイドするデバイスとしても機能します．依存型は型駆動開発を強力に推し進める力を持っています．

依存型は70年代に提案されたアイデアですが，今も様々なかたちで発展しています．依存型プログラミングが難しいと言われる理由の一つに，型記述に式が現れるために「同じ型とは何か」を扱いづらいということが挙げられます．型の同一性を適切に扱うための型理論の拡張として Homotopy Type Theory があり，それに計算的意味（computational meaning）を与える，いわば HoTT に実装を与えるものとして Cubical Type Theory があります．2019年に発表された Cubical Agda は，依存型付きプログラミング言語 Agda の拡張であり，Cubical Type Theory をサポートしています．

このたびのPPLサマースクールでは，現代的なプログラミングにおいてますます重要な概念となっている依存型を題材として取り上げ，依存型への入門から，その理論的発展までを，依存型を持つプログラミング言語である Agda を通して体験的に理解できる機会を提供します．本サマースクールでは，お二人の専門家を講師としてお招きし，ご講演いただきます．

↑

講師紹介（発表順） †

叢 悠悠（東京科学大学）

東京科学大学情報理工学院数理・計算科学系助教．2019年お茶の水女子大学大学院博士後期課程修了．型システムの理論と応用に関する研究を行う．

上村 太一（名古屋大学）

名古屋大学大学院情報学研究科特任助教．2021年アムステルダム大学にて博士号取得．高次元圏論的型理論の研究を行う．

↑

プログラム †

第1部：依存型付きプログラミング言語Agda，および，依存型を用いたプログラミング（講師：叢 悠悠）

第2部：依存型の拡張としてのホモトピー型理論，Cubical Type Theory，および，Cubical Agda（講師：上村 太一）

（プログラムの詳細は追ってお伝えします）

↑

参加費・参加申し込み †

TBA

↑

問い合わせ先 †

PPLサマースクール2025 幹事
川端 英之（広島市立大学）
E-mail: kawabata[at]hiroshima-cu.ac.jp

↑

過去のサマースクール †