Counterexample-guided Abstraction Refinement，简称为 CEGAR 算法，通过将多个状态合并，并仅在需要时进行细化，从而减少状态空间的大小，改善了模型检查中状态爆炸的问题。

本文简述了论文 Synthesis of Reactive(1) designs 中讲到的程序综合算法。

从历史角度帮助我们更好地猜一个词是 en 词还是 ett 词

本文介绍了原始递归函数及其计算能力。

本文介绍了 LTL 的一种扩展：带过去信息的 LTL

本文介绍了 χ 语言如何转化到无类型 lambda 演算。

介绍两种定义实数的方式：戴德金分割和柯西序列，并讨论它们的等价性

介绍分离逻辑解决了 Hoare Logic 的什么问题，并介绍分离逻辑相关的概念与证明规则

本文讲解了 Büchi 自动机、 ω-正规语言 和 ω-正则表达式 的概念和 Büchi 自动机 与 ω-正则表达式 之间的互相转换算法。

本文讲解了下推自动机的概念。