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

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 reductions 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 untyped lambda calculus

Backmatter

• Acknowledgements
• Fonts: Test page for fonts
• Statistics: Line counts for each chapter

Related

• Mailing lists for PLFA:
  • 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 (please tell us of others):
  • Philip Wadler, University of Edinburgh, 2018, 2019
  • David Darais, University of Vermont, 2018
  • John Leo, Google Seattle, 2018–2019
  • Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), 2019
  • Prabhakar Ragde, University of Waterloo, 2019
  • Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup 2019–2020
  • Dan Ghica, University of Birmingham 2019
  • Jeremy Siek, Indiana University, 2020
  • William Cook, University of Texas, 2020
• Shortlisted for Outstanding Course by Edinburgh University Student Association (second place) 2020
  • “Types and Semantics for Programming Languages was the single best course I took throughout my time at the University of Edinburgh. Philip Wadler clearly poured his heart into teaching it, including writing a whole textbook including exercises specifically for the course.”
  • “One of the most inspiring courses. Philip designed a course that is both very theoretical and very practical.”
• A paper describing the book appeared in SBMF and SCP.
• NextJournal has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.