index.md

title	layout
Table of Contents	page

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]({{ site.baseurl }}/Dedication/)
• [Preface]({{ site.baseurl }}/Preface/)
• [Getting Started]({{ site.baseurl }}/GettingStarted/)

Part 1: Logical Foundations

• [Naturals]({{ site.baseurl }}/Naturals/): Natural numbers
• [Induction]({{ site.baseurl }}/Induction/): Proof by induction
• [Relations]({{ site.baseurl }}/Relations/): Inductive definition of relations
• [Equality]({{ site.baseurl }}/Equality/): Equality and equational reasoning
• [Isomorphism]({{ site.baseurl }}/Isomorphism/): Isomorphism and embedding
• [Connectives]({{ site.baseurl }}/Connectives/): Conjunction, disjunction, and implication
• [Negation]({{ site.baseurl }}/Negation/): Negation, with intuitionistic and classical logic
• [Quantifiers]({{ site.baseurl }}/Quantifiers/): Universals and existentials
• [Decidable]({{ site.baseurl }}/Decidable/): Booleans and decision procedures
• [Lists]({{ site.baseurl }}/Lists/): Lists and higher-order functions

Part 2: Programming Language Foundations

• [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
• [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
• [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
• [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
• [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
• [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
• [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
• [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus
• [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus

Part 3: Denotational Semantics

• [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus
• [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional
• [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics
• [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics
• [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence

Appendix

• [Substitution]({{ site.baseurl }}/Substitution/): Substitution in untyped lambda calculus

Backmatter

• [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
• [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts

Related

Mailing lists

• [email protected]:
  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.
• [email protected]:
  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, Pontifícia Universidade Católica do Rio de Janeiro

2018

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

Please tell us of others!