Interesting Things

• Euclid's Elements (translated and commentated by Heath)
  Euclid uses the method of exhaustion several times in Book XII starting at proposition II, which involves generating a polygon by induction, and then using proof by contradiction to transform the statement into one about the generated polygon. Effectively, Euclid turns proof by contradiction into proof by induction two thousand years before calculus.
• The Works of Archimedes (translated and commentated by Heath)
  In Archimedes's "Measurement of a Circle", Archimedes finds π via method of exhaustion, effectively doing calculus two thousand years too early. Interestingly, Archimedes also gives out approximations for square roots like free candy.
• Computer-Aided Reasoning: An Approach and Computer-Aided Reasoning: ACL2 Case Studies
  These are books on ACL2, an automated theorem prover which defines its semantics mostly along the lines of Common LISP with tail recursion. This makes for a fairly clean semantics and prover.
• Logic Programming
  Course notes for a course on logic programming. One of the most extensive texts on logic programming as far as I know.
• Purely Functional Data Structures by Chris Okasaki
  In my opinion, this is the best book on non-graph data structures. This is a good complement to any algorithms textbook. Make sure you get the book proper and not just the thesis. The book lacks discussion on sparse arrays and hash trees, which are in my opinion the most useful data structures, but otherwise it is a solid text on data structures. If I could ask to change any textbook, I would have a new edition added to this which directly discusses hashing and hash trees specifically. This link discusses data structures that are missing from Okasaki.
• Structure and Interpretation of Computer Programs
  This is the Scheme book. It's worth reading at least the first two chapters, which cover tail recursion and data structures. The third chapter is about state, and is something that every imperative-language programmer should read. The fourth and fifth chapters are worthwhile and among the best discussions of their topics, but I'm not sure the topics themselves offer a sufficient canon even today, so I can only recommend them as starting points for programming languages and compilers respectively.
• A Problem Course in Compilation: From Python to x86 Assembly
  In my opinion, the best introductory "textbook" available today. Textbook is in quotes because these are actually course notes for CSCI 4555 at CU Boulder, which I took as an undergraduate at CU Boulder. The course has you start building a compiler immediately, and provides emphasis on the most important topics rather than trying to cover absolutely everything.
• Compiling with Continuations by Andrew Appel
  I think this is the best non-introductory textbook for compilers. Constraining ABIs and SSA's popularity has prevented continuation-based compilation from becoming even a common method for writing compilers, and this textbook is a casualty. If you want to understand how to compile functional programming languages, just read this.
• Modern Compiler Implementation in ML
  An introductory textbook by the same author as Compiling with Continuations. This covers a more typical compilation process, and is effectively the standard introductory compiler textbook, and a good complement to compiling with continuations.
• The Little Books
  Short books with some interesting ideas. The books are good starting points for Scheme, logic programming (The Reasoned Schemer) and proving programs with ACL2-style proofs (The Little Prover). Most recently there's a book on dependent types (The Little Typer) which I haven't read.
• Software Foundations
  A series of books about logic and programming. I read most of the first book when the series was just a fairly lengthy single book called "Software Foundations". I'm really recommending just the first book, "Logical Foundations", since that's what I've read. This made implementing the first book
• Types and Programming Languages
  The canonical textbook on type theory in programming languages. I'm not a fan of type theory myself, but anyone who wants to understand it should read this.