# Liam's Books

## Table of Contents

This is a non-exhaustive list of books that I have and recommend, related to various theoretical topics covered in this course and others.

As I own most of these books, I am able to lend some of them out on request. Please contact me for details.

## 1 Programming Languages

### 1.1 General Books

**Types and Programming Languages**
*Pierce*

A thorough introduction to the syntax and semantics of programming languages, particularly type systems. The basis of a lot of material for this course. Often recommended to newcomers to programming language theory.

**Practical Foundations for Programming Languages**
*Harper*

An excellent-quality book that is highly comprehensive and covers large amounts of the material in this course. Does assume a certain level of mathematical maturity though.

**Advanced Topics in Types and Programming Languages**
*Pierce (ed.)*

A collection of chapters written by different leading experts on advanced topics in type systems such as substructural (linear) types, dependent types, and constraint-based type inference. Continues on from Types and Programming Languages, so it would be wise to refer to that also.

### 1.2 Semantics

**Formal Semantics of Programming Languages**
*Winskel*

A commonly-recommended text that goes into the more traditional semantics techniques for programming languages, such as denotational semantics based on cpos and domain theory. I find this one quite dense.

**Semantics of Programming Languages: Structures and Techniques**
*Gunter*

Another book that discusses models and denotational semantics in a lot more detail than COMP3161. I have yet to work through this one fully.

### 1.3 Theorem Proving about PLs

**Concrete Semantics**
*Klein, Nipkow*

One of the co-authors is a lecturer for COMP4161. Teaches programming language theory and semantics via the Isabelle proof assistant. The first half is mostly about theorem proving in Isabelle, and the second half is mostly on PL theory.

**Sofware Foundations**
*Chlipala*

A similar book to Concrete Semantics, except using the Coq theorem prover rather than Isabelle.

## 2 Lambda Calculus

**Lambda Calculus and Combinators**
*Hindley, Seldin*

A nice guide to λ calculi and combinator calculi, their properties, and type systems for them. Fairly easy to follow and lots of helpful exercises with solutions.

**The Lambda Calculus: its Syntax and Semantics**
*Barendregt*

An extremely thorough tome about untyped λ calculus. Brings together basically all current knowledge about this fascinating formalism. Very comprehensive.

**Lambda Calculus with Types**
*Barendregt*

A similarly comprehensive tome to Barendregt's other work, this time about typed λ calculus.

## 3 Functional Programming

**Thinking Functionally with Haskell**
*Bird*

A great introduction to Haskell programming with emphasis on the *computer scientist* approach.
Equational reasoning is emphasised throughout, and the careful, mathematical construction of
programs is recommended. Excellent exercises and a good introduction to Haskell.

**Pearls of Functional Algorithm Design**
*Bird*

Continuing on from Bird's Haskell introduction, this book describes how to design and optimise many algorithms using equational reasoning and functional programming. The techniques described are beautiful and convey a lot of why functional programming can be nice for writing programs.

**Purely Functional Data Structures**
*Okasaki*

An invaluable book for a functional (or concurrent) programmer, describing data structures that have good complexity and also do not rely on any destructive update. Example code is given in both OCaml and Haskell.

## 4 Compiler Implementation

**Modern Compiler Implementation in ML**
*Appel*

A nice book that discusses more modern techniques for compiler design, including more advanced language features than the more popular "dragon book" covers, using a suitably functional language.

**Compilers: Principles, Techniques, and Tools**
*Aho, Sethi, Ullman*

The famous "dragon book" for compiler implementation. Explains a lot of traditional parsing methods and code generation.

## 5 Mathematics

### 5.1 Foundations of Mathematics

**Practical Foundations of Mathematics**
*Hunter*

One of the best books to introduce mathematical foundations based on λ calculus and type theory, rather than formalistic axioms and Hilbert-style symbol pushing. Highly recommended.

**Naive Set Theory**
*Halmos*

A very readable introduction to the set-based mathematical foundation of Zermelo and Fraenkel, without getting bogged down in formalism.

**Principia Mathematica**
*Russell, Whitehead*

Russell and Whitehead's valiant attempt to formalise all of mathematics in predicate logic. Perhaps don't try to read the whole thing - it's 3 very long volumes full of logical derivations.

**On Formally Undecidable Propositions of Principia Mathematica and Related Systems**
*Gödel*

A short, very readable proof that the previously-listed 3-volume masterwork is fundamentally flawed - that it is impossible to consistently and completely formalise all of mathematics.

### 5.2 Category Theory

**Category Theory for Programmers**
*Milewski*

An excellent introduction to all the major concepts of Category Theory, with example code in Haskell and C++ to motivate many of the constructions. Most Category Theory texts use examples from algebraic topology or other mathematical domains, so if you're looking for an introduction that doesn't rely on that, this is where to look.

**Basic Category Theory for Computer Scientists**
*Pierce*

A very short book, suitable as a quick reference guide to categorical concepts. Doesn't get very thoroughly into the fantastically useful results such as the Yoneda Lemma that result from categorical constructions.

**Category Theory**
*Awodey*

A comprehensive text on category theory, but quite dense. Still, it's where I learnt most of my category theory from.

### 5.3 Logic

**Mathematical Logic for Computer Science**
*Ben-Ari*

A nice book on traditional logics, including modal, temporal and other logics commonly found in computer science. It's a mathematics book, but the examples are motivated from CS, not math.

## 6 Formal Methods

### 6.1 Applied

**Programming: The Derivation of Algorithms**
*Kaldewaij*

A lovely text with lots of great exercises, on using Hoare Logic specifications to verify and derive program implementations.

**Programming from Specifications**
*Morgan*

A text written by one of the lecturers at this university, on deriving programs from
specifications written in a *refinement calculus*. COMP2111 students often made use of this
excellent book.

**A Discipline of Programming**
*Dijkstra*

A famous monograph where one of the great contributors to formal methods explains his weakest-precondition calculus as a means of deriving and verifying programs, while also philosophically justifying the case for formal methods in the first place.

### 6.2 General

**Foundations of Program Verification**
*Loeckx, Sieber*

A very dense summary of many verification techniques, including Floyd, Hoare and Dijkstra's methods. Backs it up with formal semantics in a denotational style. Not for the faint of heart.

### 6.3 Specific Domains

**Data Refinement: Model-oriented proof methods and their comparison**
*de Roever, Engelhardt*

A great book that unifies all the various different techniques for *data refinement* (the act
of replacing an abstractly-defined data type with a more concrete one) into one semantic
framework based on simulation relations. COMP2111 students would have some exposure to this.

**Concurrency Verification**
*de Roever*

Another excellent book that encompasses many of the standard ways to prove properties about concurrent programs and systems. Formed the basis of a lot of COMP3151.

## 7 Algorithms and Complexity Theory

**Introduction to Algorithms**
*Cormen, Leiserson, Rivest, Stein*

The standard encyclopaedic text on algorithms, their complexity, and their motivation. Can't really go wrong with this one. I've referred to it many times. COMP3821 or 3121 students will likely have seen it before.

**Introduction to the Theory of Computation**
*Sipser*

A great textbook on the three topics of automata theory, computability theory, and complexity theory (and the relationship between them). The main textbook for COMP4141. I really love the way proofs and exercises are presented in this book.

**Computational Complexity**
*Papadimitriou*

A more thorough text than Sipser on the area of complexity theory in particular, although there is quite a lot of errata in this book (typos etc.) and they haven't published a newer edition.

## 8 Other

**Principles of Concurrent and Distributed Programming**
*Ben-Ari*

The other textbook commonly used in COMP3151. Outlines many of the approaches for concurrent and distributed programming, including shared memory problems (e.g. critical sections), message passing, and distributed systems problems like fault-tolerance in the presence of byzantine or crash failures.