#函数式编程
计算概论期末复习笔记（Bird Meertens 形式开始的部分）
主要包含使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。
这是本课程的最后一个部分，同时可能是在上半学期和下半学期前部的铺垫下真正想讲的东西。其中函数式编程的想法提供了无副作用的函数和高阶函数的例子，从而能够被我们讨论；定理证明器则允许我们验证推导的正确性。…
【Agda 语言】形式化证明所需的主要设施
类型论的实践：函数式程序推理与演算。Agda 中的证明、归纳、列表、Internal Verification 和等式理论。
【Haskell 语言】单子与副作用
函数式语言如何引入副作用：函子、应用函子、单子。
【Haskell 语言】基础概念与语法
函数式语言的基础特性概览：列表、类型与高阶函数。
无类型 λ 演算
最经典的类型论例子：无类型 λ 演算的规则、使用和合流性。