#计算理论
Bird Meertens 形式与高效程序导出
主要包含使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。
这是本课程的最后一个部分，同时可能是在上半学期和下半学期前部的铺垫下真正想讲的东西。其中函数式编程的想法提供了无副作用的函数和高阶函数的例子，从而能够被我们讨论；定理证明器则允许我们验证推导的正确性。…
Agda 语言与基本的形式化证明
下半学期使用 Agda 来讲授函数式程序推理与演算，也展示了 Internal Verification 思想。…
Haskell 的单子与副作用
函数式语言如何引入副作用：函子、应用函子、单子。
LISP 模式：图灵完备及元编程
在 1960 年，John McCarthy 中一篇论文中定义了一个名为 Lisp（意为 list processing）的编程语言。Paul Graham 认为，“目前为止只有两种真正干净利落，始终如一的编程模式：C 语言模式和 Lisp 语言模式。此二者就像两座高地……随着计算机变得越来越强大，新开发的语言一直在坚定地趋向于 Lisp 模式。”
Lisp 似乎受到了 Lambda 演算与 Kleene 的递归论的影响，但不完全来自于它们。…
无类型 λ 演算与重写系统
本文讨论 Alonzo Church 发明的无类型 λ 演算 Lambda Calculus. 这是一个类型论与函数式编程的基础模型。…