PLMW 演讲：元理论的机械化
可惜了，youtube version 最后没被上传。就凑合着看吧。
个人无法翻译 Mechanizing Metatheory。这一般是指用 定理证明器 形式化某个元理论。
动机
元理论是指讨论关于一个理论本身的性质。比如说我们想证明所有通过Java类型检查和证明的程序不会出现运行时的Null Exception这样一个定理，（曾经是错的现在不知道怎么样了），这样的定理是讨论Java类型系统本身的，所以被称作元定理。
一般来说这样的定理是用纸笔/Latex做做证明的。但是从Proof Engineering的角度来看，这样在Latex上的定义、定理没什么扩展性，而且细节容易掉进犄角旮旯里而导致某些错漏，加之没有定理证明怎么能相信你的证明呢（（
现有问题
然而，使用定理证明器需要大量的训练和经验。最简单的例子：元理论中，在论文里面你可以省略对于变量操作（例如变量替换，自由变量提取）的细节。然而对电脑来说，这类操作必须严谨完整的写出来；而且这些操作本身会有一些trivial的性质。比如说 $X[a \mapsto c][b \mapsto d] = X[b \mapsto d] [a \mapsto c]$ 亦即在某些简单的情况下可以交换替换顺序 这个定理就要被完整的在定理证明器中递推的证明一遍。只是考虑这些变量就耗费大量的精力去证明相关的Lemma。
仅仅考虑变量本身，在定理证明器中就有多种设计模式可以参考。 Pientka 主要是考虑 HOAS (Higher-order Abstract Syntax) 和 Contextual Modal Type Theory。
HOAS
简单来说, HOAS是一个用于 将 程序本身 表达成 数据结构 的 设计模式。比如说我们用简单的代数数据类型/BNF 表达一个程序 tm := var | Lam var tm | App tm tm 。这里的Lam还是用一个简单的tuple表达的。现在我们考虑写一个替换函数，可以想象这个函数不断的递归分解每个子结构。然后我们会需要 capture-avoiding substitution, 亦即考虑同名变量的shadowing问题。
然而如果我们用HOAS的话， 这个Lam就会直接存一个函数本身 fun var => tm， 亦即这次我们用一个函数作为数据结构的一部分。这就是Higher-order的意思。
这样做的话，好处是 – 替换函数做 capture-avoiding substitution 会简单一点 (alpha-renaming)，直接把传入这个函数一个term即可 ； 坏处是 – 我们有一个函数作为数据的一部分，解构这个数据本身有点复杂，尤其是在定理证明器中使用HOAS的时候（这里可能有点争议，可能参考Pientka的演讲和CPDT会更好）。
然而在定理证明器中使用HOAS不是那么容易，因为定理证明器有Strict Positivity的限制。去解决这个问题，我们有很多种办法。Pientka研究的是使用Contextual Type Theory解决这个问题，结合 LF 和 MLTT 的优点。这个演讲中有更细致的讨论，但需要不少的LF + MLTT基础。
Calculating Dependently-Typed Compilers
by Pickard and Hutton
这里的”计算”是指什么？
这里的计算是指 “根据规范系统地导出 可证明正确 的编译器实现”。举个例子，假如我们要写一个Scheme编译器，我们需要参考某个官方的Scheme Reference Manual,例如 R6RS。这样做的原因是因为，当程序员编程的时候，应该是根据某个标准编程而不是某个实现。比如说GCC和Clang作为不同的C编译器，可能各自实现了不同的非标准的C语言拓展。哪某个程序员如果紧贴着GCC实现，就没法轻易的用Clang/LLVM作为编译器 – 哪如果某个学术、实验级的optimization technique只在LLVM上被实现了，如果这个程序员想要使用这个优化，就头疼了。这个可以看作是某种”可移植性”，也可以看作是”数学定义的必要性”。
然而，R6RS是一个几乎用人类语言写成的reference manual，这样我们依旧没法”系统地导出”某个实现。我们需要某个更形式的对Scheme语言的（数学）定义。这类定义一般是由 操作语义 或者 其他形式语义 写成的。既然这是一个数学定义，我们就有可能从这个语义”系统地导出”（或者说”算出”）一个解释器、编译器的实现。（实际上，我们可以直接把一个解释器看作一个大步操作语义（某种程度来说，就像是实现即规范。））
这样的计算和”首先我们在定理证明器中写一个编译器，然后证明这个实现满足了规范”是不同的。
解释器可以系统地生成编译器。其实这也和 “正确性” 相关。如果一个编译器和解释器行为一致，哪我们就可以说这个编译器是正确的，（当然前提是这个解释器自己就是一个大步操作语义）。形式化的说，
(exec (compile e) s) = eval e s
eval 是定好的解释器，s是栈，compile 就是我们想要的编译器，exec就是编译后代码的执行器（这也由我们决定）。
之前的工作是写一个 动态类型语言的编译器。这次的工作是一个静态类型语言的编译器，作者选择使用依值类型语言Agda作为实现编译器的实现平台/元语言。
为什么用依值类型？ 为什么用Agda?
我们可以使用依值类型去记录操作的语言的类型信息（还有栈上的类型信息）.
- 使用依值类型作为元语言可以直接用元语言的类型检查来做到对象语言的类型检查。这里的意思说，假设我们用Agda来写Java的编译器，那么我们可以做到在Agda内定义数据的时候使用依值类型，那么Java的源程序，作为IR数据存在Agda内会需要符合定义 – 依值类型的强大之处在于可以让这些IR数据直接被静态类型检查了（不会有ill-typed的程序作为数据的一部分）这相当于直接类型检查
- 同样的检查可以用于静态检查 栈的信息
是怎么算的呢？
我们需要根据那个正确性条件实现编译器。所以从某种角度来说，我们需要解以下方程
(exec (compile e) s) = eval e s
未知量是 exec, compile 还有 compile的输出的类型(栈的指令的数据结构也是由我们定义的)。为了解这个方程，我们对e做结构递归（因为源语言已经被定好了），然后对每一个不同的表达式我们都要得到正确的exec,compile 的”反应”。
更详细的信息在论文里可以看见；而且论文中的源语言还支持更多更高级的特性。
Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation),
presented by LambdaMan
如果读者不了解 HoTT （不理解为什么同一个等号的命题可以有多个证明而且我们会在乎这些证明是不是相等）以及 parametricity/logical relation (LR)/theorem for free!, 这个论文和这个演讲真的不太能读懂。然而LR这个东西很难讲清楚/讲好，难讲到让我怀疑Progress and Preservation是不是PL界走上的弯路 – 因为如果从最初就没有Syntactic Type Safety, 哪LR可能会在本科PL就教，可能这个理论会被简化到早就可以被轻松的理解了。
这个演讲 讲了什么是 Leibniz Equality，但是对 Martin Lof Identity Type 讲的不够清楚。如果感兴趣我建议读读 HoTT，当然定义是非常简单的但是定义是怎么来的并不简单。附上的链接是Harper的课，可能不够数学但是足够CS了。当然可能也需要一些定理证明器的基础。