目录
本书是 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。欢迎拉取请求。 GitHub 上有带有习题答案的私有仓库。如果你想要获取访问权限，请联系作者之一。
前言
- Dedication: 题献
- Preface: 前言
- 使用说明
第一分册：逻辑基础
- Naturals: 自然数
- Induction: 归纳证明
- Relations: 关系的归纳定义
- Equality: 相等性与等式推理
- Isomorphism: 同构与嵌入
- Connectives: 合取、析取与蕴涵
- Negation: 直觉逻辑与命题逻辑中的否定
- Quantifiers: 全称量词与存在量词
- Decidable: 布尔值与判定过程
- Lists: 列表与高阶函数
第二分册：编程语言基础
- Lambda: λ-演算简介
- Properties: 进行性与保型性
- DeBruijn: 内在类型的 de Bruijn 表示法
- More: 简单类型 λ-演算的更多构造
- Bisimulation: 联系不同的规约系统
- Inference: 双向类型推理
- Untyped: 完全正规化的无类型 λ 演算
- Confluence: 无类型 λ-演算的合流性
- BigStep: 无类型 λ-演算的大步语义
Part 3: Denotational Semantics
- Denotational: Denotational semantics of untyped lambda calculus
- Compositional: The denotational semantics is compositional
- Soundness: Soundness of reduction with respect to denotational semantics
- Adequacy: Adequacy of denotational semantics with respect to operational semantics
- ContextualEquivalence: Denotational equality implies contextual equivalence
附录
- Substitution: Substitution in the untyped lambda calculus
后记
相关资源
使用本书教学的课程
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
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
请告诉我们其他的资源！