COMP[39]161 Concepts of Programming Languages
Semester 2, 2018

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.

2018-11-16 Fri 19:37

Announcements RSS