ezyang’s blog

the arc of software bends towards understanding

Spring Reading: 2011 edition

Books are expensive, but by the power of higher-education (also expensive, but differently so), vast oceans of books are available to an enterprising compsci. Here’s my reading list for the spring break lending period (many of which were recommended on #haskell:

  • Concepts, Techniques, and Models of Computer Programming by Peter Van Roy and Seif Haridi. Wonderfully iconoclastic book, and probably one of the easier reads on the list.
  • Types and Programming Languages by Benjamin Pierce. I’ve been working on this one for a while; this break I’m focusing on the proof strategies for preservation, progress and safety, and also using it to complement a self-study course summed up by the next book.
  • Lectures on the Curry-Howard Isomorphism by M.H. Sørensen and P. Urzycyzn. Very good, I’ve skimmed the first three chapters and I’m working on the exercises in chapter 2. I’ve been prone to making silly mis-assertions about the Curry-Howard Isomorphism (or is it?), so I’m looking forward to more firmly grounding my understanding of this correspondence. The sections on intuitionistic logic has already been very enlightening.
  • Type Theory and Functional Programming by Simon Thompson. Haven’t looked at it yet, but fits into the general course of the previous two books.
  • Purely Functional Data Structures by Chris Okasaki. Also one I’ve been working on a while. Working on compressing all the information mentally.
  • Basic Category Theory for Computer Scientists by Benjamin Pierce. I’ve got two items on category theory; I got this one on a whim. Haven’t looked at it yet.
  • Pearls of Functional Algorithm Design by Richard Bird. Something like a collection of puzzles. I think I will enjoy reading through them and working out the subtleties. I probably won’t get to the information compression stage this time around.
  • Category Theory by Steve Awodey. I was working on the exercises in this textbook, and think I might get past the first chapter.

3 Responses to “Spring Reading: 2011 edition”

  1. Thomas says:

    Some remarks on Curry-Howard and category theory. If you haven’t noticed yet, there is some of the material towards a categorical understanding of the Curry-Howard correspondence in Awodey’s book. Probably the best way to get a feel for Curry-Howard (probably should add Lambek as well) is to get into a routine of asking yourself what a proof for a given statement would look like constructively.

    Another book I’ve enjoyed in that regard is Crole’s “Categories for Types,” which in my opinion is written very well and is one of the most readable books dealing with category theory I’ve come across so far. An underrated book that has helped me and others a lot is “Abstract and Concrete Categories.” I like that much better than the book by Awodey (or Mac Lane for that matter). If you are interested in categorical logic, you will likely need other books though.

  2. Thanks for the pointers. I wasn’t planning on studying categorical logic but I suppose it’s a sort of logical combination of the two topics. :-)

  3. Dave B says:

    I’ve just started reading Asperti and Longo’s “Categories, Types and Structures” which is available free here:


    I’ve got Pierce’s “Types and Programming Languages” and Okasaki’s “Purely Functional Data Structures” but haven’t yet…you know…actually…emm….opened them yet! [blush]

    Keep up the superb blog!

Leave a Comment