本书是 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。欢迎拉取请求。

前言

第一分册:逻辑基础

第二分册:编程语言基础

后记

相关资源

  • Courses taught from the textbook:
    • Philip Wadler, University of Edinburgh, 2018
    • 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
  • A paper describing the book appeared in SBMF.