【締切間近】PPLサマースクール2025「依存型入門 - 基礎・応用・発展」のご案内【9/2 @ 東海大学品川キャンパス】

[川端 英之]

皆様，（重複してお受け取りになった場合はご容赦ください）
広島市立大学の川端と申します．

先日案内いたしました下記の件，申込締め切り（8月31日）が迫ってきましたので，
あらためてご案内いたします．

　　日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催，
　　PPLサマースクール2025「依存型入門 - 基礎・応用・発展」（9月2日開催）
　　http://ppl.jssst.or.jp/index.php?ss2025

本サマースクールは，日本ソフトウェア科学会第42回大会（9月3日～5日）の併設イベントです．
https://jssst2025.wordpress.com/

多くの方のご参加をお待ちいたしております．

====================================================

# PPLサマースクール2025「依存型入門 - 基礎・応用・発展」

http://ppl.jssst.or.jp/index.php?ss2025

日時：2025年9月2日(火) 10:30～17:00 (10:00受付開始)
場所：東海大学品川キャンパスおよびオンラインのハイブリッド開催
講師：叢 悠悠（東京科学大学），上村 太一（名古屋大学）

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


## 概要

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

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

　依存型は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:00 Agdaによる依存型プログラミング入門 （講師：叢 悠悠）
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 を用いたプログラミングを
通して、依存型の基本的な使用例を紹介します。また、より発展的な例
として、依存型の音楽への応用についても取り上げます。

### 第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についてやや詳しく解説する。


## 参加費

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

参加申込手続きは，日本ソフトウェア科学会第42回大会 参加申し込みページ
にて行なってください．
https://jssst2025.wordpress.com/callforpart/


## 問い合わせ先

PPLサマースクール2025 幹事
川端 英之（広島市立大学）
E-mail: kawa...@hiroshima-cu.ac.jp
______________________________________________________
川端英之＠情報工.広島市大 <kawa...@hiroshima-cu.ac.jp>

______________________________________________________
川端英之＠情報工.広島市大 <kawa...@hiroshima-cu.ac.jp>