目录
本书是 Philip Wadler 和 Wen Kokke 所著的《Programming Language Foundations in Agda》的中文翻译。
本书在线版可访问 PLFA-zh 阅读。
目前全书已翻译完毕，由于译者水平有限，错漏之处在所难免，欢迎读者提出修改建议。 如有问题可在 Issue 发起讨论或直接发起 PR。本项目源码可访问 Github 获取。
以下为原书主页内容：
本书是对编程语言理论的介绍。书中的程序使用证明助理 Agda 编写。
欢迎对本书各方面的评论和建议（章节组织，可以添加/移除的材料，解释不够清楚的部分， 有价值的习题，内容或拼写错误等）。 本书的源码托管在 GitHub。欢迎拉取请求。 GitHub 上有带有习题答案的私有仓库。如果你想要获取访问权限，请联系作者之一。
前言
- Dedication: 题献
- Preface: 前言
- 使用说明
第一分册：逻辑基础
- Naturals: 自然数
- Induction: 归纳证明
- Relations: 关系的归纳定义
- Equality: 相等性与等式推理
- Isomorphism: 同构与嵌入
- Connectives: 合取、析取与蕴涵
- Negation: 直觉逻辑与命题逻辑中的否定
- Quantifiers: 全称量词与存在量词
- Decidable: 布尔值与判定过程
- Lists: 列表与高阶函数
第二分册：编程语言基础
- Lambda: λ-演算简介
- Properties: 可进性与保型性
- DeBruijn: 内在类型的 de Bruijn 表示法
- More: 简单类型 λ-演算的更多构造
- Bisimulation: 联系不同的归约系统
- Inference: 双向类型推理
- Untyped: 完全正规化的无类型 λ-演算
- Confluence: 无类型 λ-演算的合流性
- BigStep: 无类型 λ-演算的大步语义
第三分册：指称语义
- Denotational: 无类型 λ-演算的指称语义
- Compositional: 指称语义的可组合性
- Soundness: 指称语义归约的可靠性
- Adequacy: 指称语义相对于操作语义的充分性
- ContextualEquivalence: 指称相等蕴含语境等价
附录
- Substitution: 无类型 λ-演算中的代换
后记
相关资源
使用本书教学的课程
2023
2022
- Andrej Bauer, University of Ljubljana
- Michael Shulman, University of San Diego
- Peter Thiemann, Albert-Ludwigs University
- Philip Wadler, University of Edinburgh
2021
- Favonia, University of Minnesota
- Prabhakar Ragde, University of Waterloo
- Jacques Carette, McMaster University (based on Prabhakar’s)
2020
- William Cook, University of Texas
- Maria Emilia Maietti and Ingo Blechschmidt, Università di Padova
- John Maraist, University of Wisconsin-La Crosse
- Jeremy Siek, Indiana University
- Ugo de’Liguoro, Università di Torino
2019
- Dan Ghica, University of Birmingham
- Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup
- Prabhakar Ragde, University of Waterloo
- Philip Wadler, University of Edinburgh
- Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro
2018
- David Darais, University of Vermont
- Philip Wadler, University of Edinburgh
- John Leo, Google Seattle
请告诉我们其他的资源！