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年アムステルダム大学にて博士号取得．高次元圏論的型理論の研究を行う．

↑

プログラム †

タイムテーブル

10:00 - 10:30受付
10:30 - 12:00Agdaによる依存型プログラミング入門 （講師：叢 悠悠）
12:00 - 13:30昼休み
13:30 - 15:00ホモトピー型理論および Cubical Agda (1) （講師：上村 太一）
15:00 - 15:30休憩
15:30 - 17:00ホモトピー型理論および Cubical Agda (2) （講師：上村 太一）

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

依存型を用いると、さまざまなデータや関数を正しさが保証された形で定義することができます。
本講演では、Agda を用いたプログラミングを通して、依存型の基本的な使用例を紹介します。
また、より発展的な例として、依存型の音楽への応用についても取り上げます。

受講者のみなさまへ：
可能であれば Agda をインストールした PC をご持参ください。
インストール方法は以下のページに記載されています。
https://agda.readthedocs.io/en/latest/getting-started/installation.html
また、スライドやコードは以下のリポジトリから取得してください。
https://github.com/YouyouCong/pplss-2025
（ネットワーク接続に関してはこちらの注意事項もご覧ください）

第2部：ホモトピー型理論，Cubical Type Theory，および，Cubical Agda（講師：上村 太一）

ホモトピー型理論(Homotopy Type Theory, HoTT)はUnivalence AxiomとHigher Inductive Types (HITs)によって拡張された依存型理論である。 Univalence Axiomは同値な型は区別できないという同値不変性を導く公理で、HITsはデータ型を等式を含めるように拡張する。

HoTTのプログラミング言語としての「実装」、つまりUnivalence AxiomやHITsを含む項がどう計算されるかは、Univalence Axiomの発見以来の問題であった。 Cubical Type Theoryはこの問に対する肯定的な答えで、Univalence AxiomとHITsを持ちつつcanonicityやnormalizationといった良い性質を持つ型理論である。 Cubical Type Theoryに基づく証明支援系が作られた他、既存の証明支援系であるAgdaを拡張してCubical Agdaが開発された。

本講演ではHoTTのアイディアを紹介し、Cubical Type TheoryおよびCubical Agdaについてやや詳しく解説する。

↑

参加費・参加申し込み †

PPLサマースクールの参加費は以下の通りです．

  • 一般会員：2,000円
  • 一般非会員：3,000円
  • 学生会員, 学生非会員：無料

参加申込み手続きについては，参加申込み用ページが公開されるまで，少々お待ちください．

↑

問い合わせ先 †

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

↑

過去のサマースクール †