https://plfa.github.io/

Programming Language Foundations in Agda
The Book Announcements Getting Started Citing Zhong Wen 

  * Source
  * •

Table of Contents

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

  * Dedication
  * Preface
  * Getting Started

Part 1: Logical Foundations

  * Naturals: Natural numbers
  * Induction: Proof by Induction
  * Relations: Inductive definition of relations
  * Equality: Equality and equational reasoning
  * Isomorphism: Isomorphism and Embedding
  * Connectives: Conjunction, disjunction, and implication
  * Negation: Negation, with intuitionistic and classical logic
  * Quantifiers: Universals and existentials
  * Decidable: Booleans and decision procedures
  * Lists: Lists and higher-order functions

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

  * Substitution: Substitution in the untyped lambda calculus

Back matter

  * Acknowledgements
  * Fonts

Related

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

  * William Cook, University of Texas
  * Jeremy Siek, Indiana University
  * John Maraist, University of Wisconsin-La Crosse

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, Pontificia Universidade Catolica do Rio de Janeiro

2018

  * Philip Wadler, University of Edinburgh
  * David Darais, University of Vermont
  * John Leo, Google Seattle

Please tell us of others!

  * Source
  * •

Programming Language Foundations in Agda

  * Philip Wadler
  * wadler@inf.ed.ac.uk

  *  wadler

  * Wen Kokke
  * wen.kokke@ed.ac.uk

  *  wenkokke
  *  wenkokke

  * Jeremy G. Siek
  * jsiek@indiana.edu

  *  jsiek
  *  jeremysiek

This work is licensed under a Creative Commons Attribution 4.0
International License