layout: page
title: Programming Language Theory
Programming Language Theory
Finding a path to enlightenment in Programming Language Theory can be a tough one, particularly for programming practitioners who didn't learn it at school. This resource is here to help. Please feel free to ping me or send pull requests if you have ideas for improvement.
Note that I've attempted to order the books in order of most "tackleable". So the idea is to read books from top to bottom. As always, it depends on your background and inclinations. It would be nice to provide multiple paths through this material for folks with different backgrounds and even folks with different goals. However, for now, it is what it is.
Mathematical Literacy
Algebra
Type Theory
For a quick course in Type Theory, Philip Wadler recommends: Types and Programming Languages, Proofs and Types, followed by Advanced Topics in Types and Programming Languages.
Books

PLFA  Programming Language Foundations in Agda  Philip Wadler, Wen Kokke

SF  Software Foundations  Benjamin C. Pierce et al.

TaPL  Types and Programming Languages  Benjamin C. Pierce

PROT Proofs and Types  JeanYves Girard, Yves Lafont and Paul Taylor  198790 pdf

PFPL  Practical Foundations for Programming Languages (Second Edition)  Robert Harper Online preview edition

ATTAPL  Advanced Topics in Types and Programming Languages  Edited by Benjamin C. Pierce

CPDT  Certified Programming with Dependent Types  Adam Chlipala

SEwPR  Semantics Engineering with PLT Redex  Matthias Felleisen, Robby Findler, and Matthew Flatt. Redex

HoTT  Homotopy Type Theory, Univalent Foundations of Mathematics

Coq'Art Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions  Yves Bertot, Pierre Castéran.

TTFP  Type Theory and Functional Programming  Simon Thompson, 1991

PiMLTT  Programming in MartinLöf's Type Theory, An Introduction  Bengt Nordström, Kent Petersson, Jan M. Smith
 Using, Understanding, and Unravelling The OCaml Language — An introduction pdf
 Polymorphic typing of an algorithmic language (PhD Thesis)  Xavier Leroy pdf

ATP  Handbook of Practical Logic and Automated Reasoning  John Harrison
 Basic Simple Type Theory  J. Roger Hindley pdf [email protected]

Lambda Calculus and Combinators pdf — J. Roger Hindley and Jonathan P. Seldin

Semantics with Applications: An Appetizer — Hanne Riis Nielson, Flemming Nielson
 An Introduction to Lambda Calculi for Computer Scientists  Chris Hankin
 The Definition of Standard ML (Revised)  Milner, Fofte, Harper, and MacQueen

The Definition of Standard ML (1990) and Commentary on Standard ML (1991) definition (pdf) commentary (pdf)

Programs and Proofs — Ilya Sergey pdf

Type Theory and Formal Proof: An Introduction — Rob Nederpelt, Herman Geuvers
 Lectures on the CurryHoward Isomorphism (pdf)
Papers
Videos

OPLSS — Oregon Programming Language Summer School
 OPLSS 2019 — Foundations of Probabilistic Programming and Security
 OPLSS 2018 — Parallelism and Concurrency
 OPLSS 2017 — A Spectrum of Types
 OPLSS 2016 — Types, Logic, Semantics, and Verification
 OPLSS 2015 — Types, Logic, Semantics, and Verification
 OPLSS 2014 — Types, Logic, Semantics, and Verification
 OPLSS 2013 — Types, Logic, and Verification
 OPLSS 2012 — Logic, Languages, Compilation, and Verification
 OPLSS 2011 — Types, Semantics and Verification
 OPLSS 2010 — Logic, Languages, Compilation, and Verification
 Archives 20022018
 ICFP 2012 Monday keynote. Conor McBride: Agdacurious?
Subtopics
Programming Languages
Books

DCPL  Design Concepts in Programming Languages – Franklyn Turbak and David Gifford, 2008

CTM  Concepts, Techniques and Models of Computer Programming, Peter Van Roy and Seif Haridi

EOPL  Essentials of Programming Languages, 3rd Edition  Daniel P. Friedman

PLAI2nd  Programming Languages: Application and Interpretation  Shriram Krishnamurthi course with videos PLAI1st

PAIP Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp  Peter Norvig, 1992

PLP Programming Language Pragmatics  Michael L. Scott
Papers
Compiler Construction
Books

MinCaml  A Crash Course for the MinCaml Compiler

MCIiML Modern Compiler Implementation in ML  Andrew W. Appel

pjlesterbook Implementing functional languages: a tutorial  Simon Peyton Jones and David Lester, 1992

slpjbook1987  The Implementation of Functional Programming Languages  Simon Peyton Jones  1987

MCD2e Modern Compiler Design, Second Edition — Dick Grune et al.

EaC2e Engineering a Compiler, 2nd Edition, Cooper and Torczon

Compiler Construction, Niklaus Wirth

DragonBook  "The Dragon Book" Compilers: Principles, Techniques, and Tools

LiSP  Lisp in Small Pieces  Christian Queinnec

CwC Compiling with Continuations  Andrew W. Appel

Static Program Analysis, Anders Møller and Michael I. Schwartzbach
 List of compiler books at the GCC Wiki
Papers
Videos
Runtime systems
Books
Papers
Functional Programming
Books

Bird and Wadler  Introduction to Functional Programming, 1st Edition  Bird and Wadler

AoP  The Algebra of Programming  Richard Bird, Oege de Moor

Programming in Haskell — Graham Hutton (2007)

RWH  Real World Haskell  Bryan O'Sullivan, Don Stewart, and John Goerzen

FPiS  Functional Programming in Scala  Paul Chiusano and Rúnar Bjarnason

SICP, Structure and Interpretation of Computer Programs, by Abelson, Sussman, and Sussman

PCPH  Parallel and Concurrent Programming in Haskell  Simon Marlow

RWOC  Real World OCaml  Jason Hickey, Anil Madhavapeddy, and Yaron Minsky

Developing Applications With OCaml — Emmanuel Chailloux, Pascal Manoury and Bruno Pagano (2000)

BTLS  The Little Schemer  Daniel P. Friedman, Matthias Felleisen

BTSS  The Seasoned Schemer  Daniel P. Friedman, Matthias Felleisen

BTML  The Little MLer  Matthias Felleisen, Daniel P. Friedman

The Reasoned Schemer and miniKanren

HTDP  How to Design Programs  Matthias Felleisen, Robert Findler, Matthew Flatt, Shriram Krishnamurthi

HR  The Haskell Road to Logic, Maths and Programming  2nd Ed.  Kees Doets, Jan van Eijck pdf
 A Book of Abstract Algebra  2nd Ed.  Charles C. Pinter booko
 Purely Functional Data Structures  Chris Okasaki phdthesis in pdf [email protected] More purely functional data structures
Papers

Lambda Papers  Lambda: The Ultimate Imperative/Declarative/GOTO  Guy Steele and Gerald Sussman

Exploring Generic Haskell (PhD thesis)  Andres Löh. This an epic, accessible, booklength PhD on datatype generic programming.
 ICFP accepted papers
Videos
Category Theory
Philip Wadler's advice here is "read Pierce for motivation, Mac Lane for the
presentation of the maths".
Books

Cakes, Custard and Category Theory: Easy recipes for understanding complex maths — Eugenia Cheng
 Category Theory, Steve Awodey. notes
 Basic Category Theory for Computer Scientists  Benjamin C. Pierce. Previously available in a draft entitled A taste of category theory for computer scientists

Categories for the Working Mathematician — Saunders Mac Lane

Conceptual Mathematics A First Introduction to Categories, 2nd Edition  F. William Lawere and Stephen H. Schanuel

Category Theory for the Sciences — David I. Spivak. Previously available in a draft entitled Category Theory for Scientists

CTCS2nd Category Theory for Computing Science  Michael Barr and Charles Wells CTCS1st
 Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist pdf
 Topoi, The Categorical Analysis of Logic, Robert Goldblatt Amazon

TTT  Toposes, Triples and Theories  Michael Barr and Charles Wells
 Category Theory Lectures Notes for ESSLLI  Michael Barr and Charles Wells pdf

Seven Sketches in Compositionality: An Invitation to Applied Category Theory  Brendan Fong, David I Spivak

Applied Category Theory Course  online course conducted by John Baez forum

CTFP  Category Theory for Programmers  Bartosz Milewski, created by Igal Tabachnik from series of blog posts; video lectures based on this material: part 1, part 2, part 3; pdf
Journals

TAC  Theory and Applications of Categories
Subtopics
Other collections