目录

本书是 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.

本书在线版可访问 PLFA-zh 阅读。

目前第一部分已翻译完毕，欢迎各位参与翻译和审校。详情请参考翻译规范。 由于译者水平有限，错漏之处在所难免，欢迎读者提出修改建议。如有问题可在 Issue 发起讨论或直接发起 PR。项目源码可访问 Github 获取。

以下为原书主页内容：

---

本书是对编程语言理论的介绍。书中的程序使用证明助理 Agda 编写。

欢迎对本书各方面的评论和建议（章节组织，可以添加/移除的材料，解释不够清楚的部分， 有价值的习题，内容或拼写错误等）。 本书的源码托管在 GitHub。欢迎拉取请求。

前言

• 题献 100
• 前言 100

第一分册：逻辑基础

• Naturals: 自然数 100
• Induction: 归纳证明 100
• Relations: 关系的归纳定义 100
• Equality: 相等性与等式推理 100
• Isomorphism: 同构与嵌入 100
• Connectives: 合取、析取与蕴涵 100
• Negation: 直觉逻辑与命题逻辑中的否定 100
• Quantifiers: 全称量词与存在量词 100
• Decidable: 布尔值与判定过程 100
• Lists: 列表与高阶函数 100

第二分册：编程语言基础

• Lambda: λ-演算简介 0
• Properties: 可进性与保型性 0
• DeBruijn: 固有类型的 de Bruijn 表示 0
• More: 简单类型 λ-演算的附加构造 0
• Bisimulation : 关系归约系统 0
• Inference: 双向类型推断 0
• Untyped: 无类型 λ-演算及其完整范式 0

后记

• Acknowledgements: 鸣谢 0
• Fonts: 字体测试页 0
• Statistics: 每章行数统计 0

相关资源

• PLFA 邮件列表：
  • plfa-interest@inf.ed.ac.uk:
    A mailing list for users of the book.
    This is the place to ask and answer questions, or comment on the content of the book.
  • plfa-dev@inf.ed.ac.uk:
    A mailing list for contributors.
    This is the place to discuss changes and new additions to the book in excruciating detail.
• 用本书教学的课程：
  • Philip Wadler, University of Edinburgh, 2018, 2019
  • David Darais, University of Vermont, 2018
  • John Leo, Google Seattle, 2018–2019
  • Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), 2019
  • Prabhakar Ragde, University of Waterloo, 2019
  • Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup 2019–2020
  • Jeremy Siek, Indiana University, 2020
• A paper describing the book appeared in SBMF.
• NextJournal has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.