CPS 変換の正当性の Agda による証明

石尾 千晶、山田 麗、浅井 健一

2018 年 3 月 6 日

PPL 2018 の論文
石尾 千晶、山田 麗、浅井 健一 「Agda による PHOAS を用いた CPS 変換の正当性の証明」 第20回プログラミングおよびプログラミング言語ワークショップ論文集、 17 ページ (2018 年 3 月)。 PDF
で定式化した CPS 変換の正当性の証明の Agda ファイル。
mono.agda
単相のλ計算。
poly.agda
let 多相の入ったλ計算。

This document was translated from LATEX by HEVEA.