This book is an introduction to programming language theory using the proof assistant Agda.

Comments on all matters—organisation, material to add, material to remove, parts that require better explanation, good exercises, errors, and typos—are welcome. The book repository is on GitHub. Pull requests are encouraged.

Front matter

Part 1: Logical Foundations

Part 2: Programming Language Foundations

  • Lambda: Introduction to Lambda Calculus
  • Properties: Progress and Preservation
  • DeBruijn: Intrinsically-typed de Bruijn representation
  • More: Additional constructs of simply-typed lambda calculus
  • 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

Appendix

Back matter

Mailing lists

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

Courses taught from the textbook

2020

2019

2018

Please tell us of others!