Below is a loosely-categorized collection of links to CS textbooks in a variety of areas that are freely available online, usually because they are one of the following:

- An open textbook (such as PLAI, SF, or the HoTT book)
- An older book that is out of print, for which the copyright has returned to the original author(s) (such as TTFP)
- An author’s own preprint or draft of a textbook. This includes cases where the author has made special arrangements with a publisher to host an electronic copy of a published text on their homepage while it remains in print.

Most of these I’ve only used for brief personal reference, and have not read in depth. The exceptions, those books I’ve spent considerable time with and highly recommend, are marked with asterisks.

I also include below a list of papers I consider good stand-alone introductions to certain topics, and a list of links to thorough special topics courses.

If you find one of the links below is broken or has moved, feel free to let me know.

Topics such as semantics, types, abstract interpretation, proof assistants…

- Software Foundations
- Practical Foundations for Programming Languages (draft)
- Programming in Martin-Lof’s Type Theory
- Proofs and Types
- Practical Foundations of Mathematics
- *Programming Languages: Application and Interpretation (second edition in progress)
- Semantics with Applications
- Lectures on the Curry Howard Isomorphism (draft)
- *Type Theory and Functional Programming
- *Certified Programming with Dependent Types
- Isabelle/HOL: A Proof Assistant for Higher-Order Logic
- Communicating Sequential Processes
- The Craft of Programming
- Denotational Semantics: A Methodology for Language Development
- *Lambda Calculi with Types
- Lambda Calculus with Types
- Logics and Type Systems
- Programming from Specifications
- Using Z: Specification, Refinement, and Proof
- Homotopy Type Theory
- Partial Evaluation and Automatic Program Generation
- Implementing Mathematics with The Nuprl Proof Development System
- Intuitionistic Type Theory
- Concrete Semantics
- PX: A Comuptational Logic
- Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
- *The Essence of ML Type Inference (Manuscript, Chapter 10 of ATTAPL)
- Static Program Analysis
- Principles of Programming Languages
- Alias Analysis for Object-Oriented Programs”
(Manuscript, chapter of
Aliasing in Object-Oriented Programming ) - Pointer Analysis

This portion excludes category theory, which is now its own section below.

- A Modern Formal Logic Primer
- Natural Logic (pdf)
- Algebraic Topology
- A Concise Course in Algebraic Topology
- Model Theory
- Set Theory
- An Introduction to Substructural Logics
- Mathematical Modal Logic: A View of its Evolution
- Normalization, Cut-Elimination, and the Theory of Proofs
- Logics of Time and Computation
- Mathematics of Modality
- Modal Logic and Process Algebra: A Bisimulation Perspective
- Lectures on Linear Logic
- Dynamics, Polarity, and Quantification
- Non-Well-Founded Sets

- Site Reliability Engineering
- The Site Reliability Workbook
- The Architecture of Open Source Applications project books:

- Abstract and Concrete Categories: The Joy of Cats
- Computational Category Theory
- Toposes, Triples, and Theories
- *Topoi: The Categorical Analysis of Logic (also at Project Euclid)
- Categories, Types, and Structures
- Higher Operads, Higher Categories
- Category Theory for Computing Science [pdf] (Barr’s publications)
- *-Autonomous Categories
- Categorical Logic
- Abelian Categories
- Metric Spaces, Generalized Logic, and Closed Categories
- An introduction to fibrations, topos theory, the effective topos and modest sets
- Categorical Homotopy Theory
- Category Theory for Scientists (Manuscript)
- Categorical Algebra (technically a 1965 journal article from Bull. Amer. Math. Soc., 17(1):40–106, but up on Project Euclid.
- Higher Topos Theory: Author version, arXiv version
- Basic Concepts of Enriched Category Theory
- The online journal Theory and Applications of Categories archives electronic versions of some out of print category theory textbooks: Reprints in Theory and Applications of Categories
- Category Theory for Programmers

- Implementing Functional Languages: A Tutorial
- The Implementation of Functional Programming Languages
- Shared Source CLI 2.0 Internals (shelved draft)
- Smalltalk-80: The Language and its Implementation (a.k.a. “The Blue Book”)
- The Design and Implementation of Probabilistic Programming Languages

- *A Commentary on the Sixth Edition UNIX Operating System (and UNIX v6 source code)
- Distributed Systems, 3rd Edition by van Steen and Tanenbaum
- Linkers and Loaders
- Concurrency Control and Recovery in Database Systems
- Is Parallel Programming Hard, And, If So, What Can You Do About It?
- Operating Systems: Three Easy Pieces
- The TCP/IP Guide
- Notes on Theory of Distributed Systems, CPSC 465/565 (technically notes, but in practice an excellent textbook)
- *Practical File System Design with the Be File System
- Principles of Computer System Design (Authors share second half online, first half published in print by Elsevier)
- Online Appendices to Computer Architecture: A Quantitative Approach, 5th Edition
- Foundations of Databases
- Security Engineering: A Guide to Building Dependable Distributed Systems
- Computer Networking
- Recent Advances in Networking, Volume 1
- Performance Evaluation Of Computer And Communication Systems
- The Network Calculus Book
- *Computer Networking: A Systems Approach

- Foundations of Computer Science
- Linear Programming: Foundations and Extensions
- The Design of Approximation Algorithms
- Mining of Massive Datasets
- Model-Based Machine Learning
- Natural Language Processing
- Foundations of Data Science
- The Elements of Statistical Learning: Data Mining, Inference, and Prediction
- Think Data Structures
- Think Bayes: Bayesian Statistics Made Simple
- Think Stats

- Topics in Parallel and Distributed Computing: Introducing Concurrency in Undergraduate Courses (preprint)

- Structure and Interpretation of Computer Programs (also: Unofficial PDF Ebook Reformatting, and SICP in Clojure)
- How to Design Classes (draft)
- How to Design Programs (2nd Edition)
- How to Design Programs (1st Edition)

While most of the books on this page are focused on more theoretical/foundational topics, sometimes you just need to learn a programming language or look at some reference on a particular language feature.

- Scala
- Programming in Scala (first edition)
- Creative Scala

- OCaml
- Haskell
- *Real World Haskell
- Parallel and Concurrent Programming in Haskell (on O’Reilly Safari, but can be read without account or subscription)
- Learn You A Haskell
- Developing Web Applications with Haskell and Yesod

- Standard ML
- Scheme and LISP
- Practical Common Lisp (and PCL in Clojure)</li>
- On Lisp
(+ one
two

three ports to Clojure)

- Erlang
- JavaScript
- Go
- Java
- Python

Some of the books listed in other categories are appropriate for someone looking to get started with programming and/or computer science. I’ve duplicated those links in this section so they’re easier to find if that’s what you need.

- Structure and Interpretation of Computer Programs
- How to Design Programs (2nd Edition)
- How to Design Programs (1st Edition)
- Creative Scala

- Abstract Interpretation (Classic): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Cousot and Cousot, POPL’77.
- Abstract Interpretation (Semantic): Abstracting Abstract Machines. Van Horn and Might, ICFP’10.
- Denotational Semantics: The Denotational Semantics of Programming Languages. Tennent, CACM 19(8), 1976.
- Program Synthesis: Dimensions in Program Synthesis. Gulwani, PPDP’10.
- Type Theory: Introduction to Type Theory. Herman Geuvers, notes from lecture given at Language Engineering and Rigorous
- Software Development run of ALFA summer school, 2009.

- Matt Might’s Grad Student Recommendations
- Various Books on Category Theory
- Benjamin Pierce’s Great Works in Programming Languages collection
- Karl Crary’s Classic Papers in Programming Languages and Logic course
- Patrick Cousot’s Abstract Interpretation course (readings section)
- Matthias Felleisen’s History of Programming Languages course readings
- Viktor Vafeiadis and Derek Dreyer’s course on Concurrent Program Logics
- Frank Pfenning’s course on Linear Logic
- Michael Shulman’s seminar on Homotopy Type Theory
- Bob Harper’s course (with videos) on Homotopy Type Theory