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

前言

第一分册:逻辑基础

第二分册:编程语言基础

  • Lambda: λ-演算简介
  • Properties: Progress and Preservation
  • DeBruijn: 内在类型的 de Bruijn 表示法
  • More: 简单类型 λ-演算的更多构造
  • Bisimulation: Relating reduction systems
  • Inference: Bidirectional type inference
  • Untyped: Untyped lambda calculus with full normalisation
  • Confluence: Confluence of untyped lambda calculus
  • BigStep: Big-step semantics of untyped lambda calculus

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

附录

后记

相关资源

邮件列表

  • 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.

使用本书教学的课程

2021

2020

2019

2018

请告诉我们其他的资源!