Skip to content

Latest commit

 

History

History
82 lines (69 loc) · 4.37 KB

index.md

File metadata and controls

82 lines (69 loc) · 4.37 KB
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

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:
    • [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:
    • 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
    • Jeremy Siek, Indiana University, 2020
  • A paper describing the book appeared in SBMF.
  • NextJournal has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.