PPL 2026 論文

田村 優衣、浅井 健一
「shift0/reset0 入りの型付き言語における CPS 変換の正当性の証明」
第２８回プログラミングおよびプログラミング言語ワークショップ論文集、
15 ページ (2026 年 3 月)。

で行った証明のソースコード。

Readme.txt        : このファイル
all.agda          : 全体をまとめたファイル

DS.agda           : DS 言語の定義
CPS.agda          : CPS 言語の定義
DS-CPS.agda       : CPS 変換の定義
Reflect3.agda     : 正当性の証明

証明環境：
	Agda 2.8.0
	standard library 2.3