• 带记录和子定型的简单类型化λ演算 • 等式理论和语义模型 • 递归类型的子定型和递归记录作为对象的模型

• 递归函数和不动点算子，以及PCF语言的编程实例 • 基于完全偏序集合的，带不动点算子的类型化λ演算的论域理论模型 • 不动点归纳法，这是一种对递归定义进行推理的证明方法

– 带依赖类型的演算，包括依赖积与依赖和 – 概要介绍Dependent ML（DML），以此来展示怎样把依赖类型用到实际语言中，这是当前程序设计语言研究的一个课题 – 带广义积与广义和的直谓式演算，以及它们同SML及其相近语言的模块系统的联系

– 代数项和它们在多类别代数中的解释 – 等式规范（也叫代数规范）和等式证明系统 – 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） – 代数之间的同态关系和初始代数 – 数据类型的代数理论 – 从代数规范导出的重写规则（操作语义）

-λ表示法和λ演算系统概述 -类型和类型系统的扼要讨论 -基于表达式的归纳、基于证明的归纳和良基归纳

中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第6章 递归类型

中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第2章 泛代数和代数数据类型

中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第1章 引言

• 类型推断的一般框架 –基于从类型化语言到无类型语言的“擦除”函数 • 加了类型变量后的→类型推断 –包括主定型和合一问题 • 带多态声明的 let的类型推断算法

• 函数式程序 –不含赋值或其它形式的改变变量值的操作 • 命令式程序 –赋值语句是典型的构造 • 本章围绕一个叫做Kernel的简单的命令式语言来讨论语义