Algebra of programming in Agda: dependent types for relational program derivation

中文摘要：

關係式程式推導（relational program derivation）是「以代數規則將關係式規格（relational specification）逐步特化為程式」的技巧。因為建構過程的保證，如此得到的程式必然是正確的。另一方面，依值型別理論（dependent type theory）已發展得十分豐富，足以表達多種正確性質且可透過型別檢驗加以驗證。

我們造了一套程式庫 AoPA，使用者可在支援依值型別的程式語言 Agda 中編寫關係式推導。每個程式都附帶一個代數推導，由型別系統擔保其正確性。

我們提出兩個有意思的例子：一個最佳化問題和快速排序的推導，後者用良基遞迴（well-founded recursion）在支援歸納式型別（inductive types）的語言中模映「計算終必停止的生滅式」（terminating hylomorphisms）。

嘔，好噁心的翻譯（特別是把所有名詞都譯出來之後 ─「生滅式」還滿惡搞的 XD）。要看原文摘要和 paper 請到 scm 老師的官方網頁。

--
是太久沒翻譯還是這段本來就難譯啊？不知道這個問題的答案代表可能是前者 XD。