Agda 中的编程语言基础

# 《Agda 中的编程语言基础》– 目录 来源：https://plfa.github.io/ 本书是一本使用证明助手 Agda\ 来介绍编程语言理论的著作。 欢迎就各方面提出意见——包括组织结构、需要增删的内容、需要更好解释的部分、优秀的习题、错误和错别字。本书仓库位于 GitHub (https://github.com/plfa/plfa.github.io/)\，欢迎提交 Pull Request。在 GitHub 上还有一个包含部分问题解答的私有仓库，如需访问，请联系作者之一。 ## 前言 - 献词 (https://plfa.github.io/Dedication/) - 前言 (https://plfa.github.io/Preface/) - 入门指南 (https://plfa.github.io/GettingStarted/) ## 第一部分：逻辑基础 - 自然数 (https://plfa.github.io/Naturals/)：自然数 - 归纳法 (https://plfa.github.io/Induction/)：归纳证明 - 关系 (https://plfa.github.io/Relations/)：关系的归纳定义 - 等式 (https://plfa.github.io/Equality/)：相等与等式推理 - 同构 (https://plfa.github.io/Isomorphism/)：同构与嵌入 - 联结词 (https://plfa.github.io/Connectives/)：合取、析取与蕴含 - 否定 (https://plfa.github.io/Negation/)：否定，涵盖直觉主义逻辑与经典逻辑 - 量词 (https://plfa.github.io/Quantifiers/)：全称量词与存在量词 - 可判定性 (https://plfa.github.io/Decidable/)：布尔值与判定过程 - 列表 (https://plfa.github.io/Lists/)：列表与高阶函数 - Lambda 演算 (https://plfa.github.io/Lambda/)：Lambda 演算导论 - 性质 (https://plfa.github.io/Properties/)：前进性与保持性 - De Bruijn (https://plfa.github.io/DeBruijn/)：内在类型的 de Bruijn 表示 - 进阶内容 (https://plfa.github.io/More/)：简单类型 Lambda 演算的其他构造 - 双模拟 (https://plfa.github.io/Bisimulation/)：关联归约系统 - 类型推断 (https://plfa.github.io/Inference/)：双向类型推断 - 无类型 (https://plfa.github.io/Untyped/)：带完全范式化的无类型 Lambda 演算 - 合流性 (https://plfa.github.io/Confluence/)：无类型 Lambda 演算的合流性 - 大步语义 (https://plfa.github.io/BigStep/)：无类型 Lambda 演算的大步语义 ## 第三部分：指称语义 - 指称语义 (https://plfa.github.io/Denotational/)：无类型 Lambda 演算的指称语义 - 组合性 (https://plfa.github.io/Compositional/)：指称语义是组合式的 - 可靠性 (https://plfa.github.io/Soundness/)：归约相对于指称语义的可靠性 - 充分性 (https://plfa.github.io/Adequacy/)：指称语义相对于操作语义的充分性 - 上下文等价 (https://plfa.github.io/ContextualEquivalence/)：指称相等蕴含上下文等价 ## 附录 - 替换 (https://plfa.github.io/Substitution/)：无类型 Lambda 演算中的替换 ## 后记 - 致谢 (https://plfa.github.io/Acknowledgements/) - 字体 (https://plfa.github.io/Fonts/) ### 使用本教材开设的课程 #### 2026 - Jeremy Siek，Indiana University (https://jsiek.github.io/PLFA-Spring-2026/) - Peter Thiemann，Albert-Ludwigs University (https://proglang.github.io/teaching/26ss/eopl.html) #### 2025 - Peter Thiemann，Albert-Ludwigs University (https://proglang.github.io/teaching/25ss/eopl.html) - Joseph Eremondi，University of Regina (https://www2.cs.uregina.ca/~eremondj/) #### 2024 - Philip Wadler，University of Edinburgh (https://plfa.github.io/TSPL/2024/) #### 2023 - Peter Thiemann，Albert-Ludwigs University (https://web.archive.org/web/20240208112146/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2023ws/) - Philip Wadler，University of Edinburgh (https://plfa.github.io/TSPL/2023/) #### 2022 - Andrej Bauer，University of Ljubljana (https://web.archive.org/web/20220222095923/https://www.andrej.com/zapiski/ISRM-LOGRAC-2022/00-introduction.html) - Michael Shulman，University of San Diego - Peter Thiemann，Albert-Ludwigs University (https://web.archive.org/web/20220810154516/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2022ss/) - Philip Wadler，University of Edinburgh (https://plfa.github.io/TSPL/2022/) #### 2021 - Favonia，University of Minnesota - Prabhakar Ragde，University of Waterloo (https://web.archive.org/web/20210424214202/https://cs.uwaterloo.ca/~plragde/747/) - Jacques Carette，McMaster University (https://github.com/JacquesCarette/CAS706-F2021/)（基于 Prabhakar 的课程） #### 2020 - William Cook，University of Texas (https://web.archive.org/web/20220101114527/https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf) - Maria Emilia Maietti 与 Ingo Blechschmidt，Università di Padova (https://web.archive.org/web/20220810154713/https://www.math.unipd.it/~maietti/typ21.html) - John Maraist，University of Wisconsin-La Crosse (https://web.archive.org/web/20220810155032/https://github.com/jphmrst/PLC/tree/fall2020#readme) - Jeremy Siek，Indiana University (https://web.archive.org/web/20220421134334/https://jsiek.github.io/B522-PL-Foundations/) - Ugo de'Liguoro，Università di Torino #### 2019 - Dan Ghica，University of Birmingham (https://web.archive.org/web/20210126123738/https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/) - Adrian King，San Francisco Types, Theorems, and Programming Languages Meetup (https://meet.meetup.com/wf/click?upn=ZDzXt-2B-2BZmzYir6Bq5X7vEQ2iNYdgjN9-2FU9nWKp99AU8rZjrncUsSYODqOGn6kV-2BqW71oirCo-2Bk8O1q2FtDFhYZR-2B737CPhNWBjt58LuSRC-2BWTj61VZCHquysW8z7dVtQWxB5Sorl3chjZLDptP70L7aBZL14FTERnKJcRQdrMtc-3D_IqHN4t3hH47BvE1Cz0BakIxV4odHudhr6IVs-2Fzslmv-2FBuORsh-2FwQmOxMBdyMHsSBndQDQmt47hobqsLp-2Bm04Y9LwgV66MGyucsd0I9EgDEUB-2FjzdtSgRv-2Fxng8Pgsa3AZIEYILOhLpQ5ige5VFYTEHVN1pEqnujCHovmTxJkqAK9H-2BIL15-2FPxx97RfHcz7M30YNyqp6TOYfgTxyUHc6lufYKFA75Y7MV6MeDJMxw9-2FYUxR6CEjdoagQBmaGkBVzN) - Prabhakar Ragde，University of Waterloo (https://web.archive.org/web/20220103155952/https://cs.uwaterloo.ca/~plragde/842/) - Philip Wadler，University of Edinburgh (https://plfa.github.io/20.07/TSPL/2019/) - Philip Wadler，Pontifícia Universidade Católica do Rio de Janeiro (https://plfa.github.io/20.07/PUC/2019/) #### 2018 - David Darais，University of Vermont (https://web.archive.org/web/20190324115921/https://david.darais.com/courses/fa2018-cs295A/) - Philip Wadler，University of Edinburgh (https://plfa.github.io/19.08/TSPL/2018/) - John Leo，Google Seattle ### 衍生作品 - PLFArend (https://github.com/marat-rkh/PLFArend)：将 PLFA 书中所有代码片段用 Arend\ 重写的版本。 - PLFaLean (https://github.com/rami3l/PLFaLean)：用 Lean 4 实现的 PLFA 证明，涵盖该书 v22\.08 版本的第二、三部分。 欢迎告知我们其他衍生作品！