目录
本书是 Philip Wadler 和 Wen Kokke 所著的《Programming Language Foundations in Agda》的中文翻译。英文原书请见 PLFA。
This is a Chinese translation of “Programming Language Foundations in Agda” by Philip Wadler and Wen Kokke。The original book is located at PLFA.
目前翻译刚刚开始，欢迎各位参与到翻译规范的拟定中。 由于译者水平有限，错漏之处在所难免，欢迎读者提出修改建议。如有问题可在 Issue 发起讨论或直接发起 PR。项目地址 PLFA-zh。
本书是对编程语言理论的介绍。书中的程序使用证明助理 Agda 编写。
欢迎对本书各方面的评论和建议（章节组织，可以添加/移除的材料，解释不够清楚的部分，有价值的习题，内容或拼写错误等）。 本书的源码托管在 GitHub。欢迎拉取请求。
前言
第一分册：逻辑基础
- Naturals: 自然数 100
- Induction: 归纳证明 0
- Relations: 关系的归纳定义 100
- Equality: 相等性与等式推理 100
- Isomorphism: 同构与嵌入 100
- Connectives: 合取、析取和蕴含 0
- Negation: 直觉逻辑与命题逻辑中的否定 0
- Quantifiers: 全称量词与存在量词 0
- Decidable: 布尔值与判定过程 0
- Lists: 列表与高阶函数 0
第二分册：编程语言基础
- Lambda: λ-演算简介 0
- Properties: 可进性与保型性 0
- DeBruijn: 固有类型的 De Bruijn 表示 0
- More: 简单类型 λ-演算的附加构造 0
- Bisimulation : 关系归约系统 0
- Inference: 双向类型推断 0
- Untyped: 无类型 λ-演算及其完整范式 0
后记
- Acknowledgements: 鸣谢 0
- Fonts: 字体测试页 0
- Statistics: 每章行数统计 0