6.2 KiB
6.2 KiB
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/)
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
- [Statistics]({{ site.baseurl }}/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.
- plfa-interest@inf.ed.ac.uk:
- Courses taught from the textbook (please tell us of others):
- Philip Wadler, University of Edinburgh, [2018]({{ site.baseurl }}/TSPL/2018/), [2019]({{ site.baseurl }}/TSPL/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]({{ site.baseurl }}/PUC/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.