CV: [pdf]

Google Scholar Author Page

ACM Author Page

DBLP

conf.researchr.org

ORCiD

Software:

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.

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

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

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

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

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)

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

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.

Scala

- Programming in Scala (first edition)
- Programming Scala

- *Real World Haskell
- Parallel and Concurrent Programming in Haskell
- Learn You A Haskell
- Developing Web Applications with Haskell and Yesod

- Practical Common Lisp (and PCL in Clojure)
- On Lisp (+ one two three ports to Clojure)

Mercurial: The Definitive Guide

Pro Git

Version Control with Subversion

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 minicourse and seminar on Homotopy Type Theory

Bob Harper's course (with videos) on Homotopy Type
Theory