本书是一本介绍函数式程序设计理论的入门读物。在内容选取上，先以λ-演算作为背景知识，然后介绍Coq和OCaml的基本用法及其主要语言特征。本书的重点是介绍函数式程序设计的基本思想和方法，让读者了解、欣赏，进而喜欢函数式程序设计。
本书共分4章：第1章介绍不带类型的λ-演算、简单类型的λ-演算和F系统，主要讨论语法和β-归约语义；第2章介绍Coq，重点从函数式程序设计的角度展开讨论，内容涉及列表、多态列表、依赖类型、高阶函数、柯里一霍华德关联及余归纳类型等；第3章介绍OCaml这门通用程序设计语言，除了基本的程序设计概念，还讨论函子和单子这样比较高级的语言特征；第4章提供了部分习题的参考答案，方便感兴趣的读者自行学习。
本书循序渐进，从基础原理到高级的语言特征，具有通俗、系统、宽广的特点，适合作为普通高等院校计算机科学和软件工程专业的本科生教学参考书，同时也可作为软件理论方向研究人员的入门读物。

第1章 λ-演算
1.1 λ-演算的起源
1.2 不带类型的λ-演算
1.2.1 语法
1.2.2 α-等价
1.2.3 替换
1.2.4 β-归约
1.2.5 表达能力
1.2.6 不动点
1.2.7 其他数据类型
1.2.8 邱奇-罗索定理
1.2.9 归约策略
1.3 简单类型的λ-演算
1.3.1 简单类型的项
1.3.2 归约
1.3.3 正规化
1.4 F系统
1.4.1 语法
1.4.2 语义
第2章 Coq
2.1 基本的函数式编程
2.2 归约规则
2.3 列表
2.4 规则归纳
2.5 多态列表
2.6 依赖类型
2.7 高阶函数
2.8 柯里-霍华德关联
2.9 归纳证明
2.10 常用证明策略
2.11 证明自动化
2.12 余归纳类型
2.13 代码抽取
第3章 OCaml
3.1 安装和使用OCaml
3.2 数据类型与函数
3.3 控制结构
3.4 高阶函数
3.5 记忆
3.6 异常
3.7 排序
3.8 队列
3.9 模块
3.10 函子
3.11 单子
第4章 部分习题参考答案
4.1 第1章练习题
4.2 第2章练习题
4.3 第3章练习题
参考文献
索引