The only resource you really need is the lecture notes. For additional background reading, you might like to consult the following, but note there will be significant differences compared to how we set things up in our unit:

  • For more on PCF, consult Chapter 2 of Mitchell’s Foundations for Programming Languages, this chapter is freely downloadable as a sample of the book.
  • If you want to learn more about this style of proof, you could try learning to use an interactive theorem prover, like Lean. These kinds of tools take the relationship between programming and proving to the next level, by giving a precisely defined programming language in which you can write your proofs, which can then be checked to be correct by the tool.
  • The ultimate reference on pure, untyped lambda calculus is Barendregt’s book The lambda calculus: its syntax and semantics, available in the library.
  • A gentler introduction, which also includes some treatment of types is Hindley & Seldin’s Lambda Calculus and Combinators: An Introduction, available in the library.
This site uses Just the Docs, a documentation theme for Jekyll.