ss2025

PPLサマースクール2025
「依存型入門 - 基礎・応用・発展」（仮題）
 
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第42回大会 併設企画
 
講師：叢 悠悠（東京科学大学）
講師：上村 太一（名古屋大学）
 
2025年9月2日(火) XX:XX〜XX:XX
東海大学品川キャンパスおよびオンラインのハイブリッド開催
このページ準備中です；内容には多少の変更がありえますが，開催日は決定しています
 

ニュース †

↑

参加者向け情報 †

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

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

概要 †

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

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

依存型は70年代に提案されたアイデアですが，今も様々なかたちで発展しています．依存型プログラミングが難しいと言われる理由の一つに，型記述に式が現れるために「同じ型とは何か」を扱いづらいということが挙げられます．そういった，equalityやhigher-dimensional structuresに対するリーズニングを行うための，依存型の拡張としての型理論に，Cubical Type Theoryがあり，それはHomotoy Type Theoryに基づいています．2020年にはCubical Type Theory に基づく依存型付きプログラミング言語 Cubical Agda が提案されています．

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

↑

講師紹介（発表順） †

叢 悠悠（東京科学大学）

TBA

上村 太一（名古屋大学）

TBA

↑

プログラム †

（暫定案）

第1部：依存型付きプログラミング言語Agda，および，依存型を活用するシステム開発事例（講師：叢 悠悠 先生）

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

↑

参加費・参加申し込み †

TBA

↑

問い合わせ先 †

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

↑

過去のサマースクール †