Electronic References

Below is a loosely-categorized collection of links to PL (and related) texts and references that are available online because they are either openly shared publications (like PLAI, SF, or the HoTT book), first editions of updated books released to the world (like Programming in Scala or Semantics with Applications), thorough but out of print references (like TTFP), or publicly available drafts (like HtDC and Practical Foundations for Programming Languages). 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.

Programming Language Theory

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

Mathematical Logic, Set Theory, Model Theory

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

Category Theory and Applications

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

Language Implementation

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)
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

General CS Theory and Algorithms

Foundations of Computer Science
Linear Programming: Foundations and Extensions
The Design of Approximation Algorithms
Mining of Massive Datasets


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

Language-Focused Introductions to Computer Science

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

Specific Programming Languages

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


OCaml Haskell Scheme and LISP Erlang JavaScript

Useful Tools

Mercurial: The Definitive Guide
Pro Git
Version Control with Subversion

Concise Overview Papers

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.

Paper Reading Lists, Courses, and Miscellaneous

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 minicourse and seminar on Homotopy Type Theory
Bob Harper's course (with videos) on Homotopy Type Theory