CSS A path to Programming Language Theory enlightenment
layout
title
page
Programming Language Theory
Programming Language Theory
Finding a path to enlightenment in Programming Language Theory can be a tough one, particularly for programming pracitioners 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.
A Survey of Modern Algebra — Birkhoff and MacLane Scribd
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
SF - Software Foundations - Benjamin C. Pierce et al.
TaPL - Types and Programming Languages - Benjamin C. Pierce
PROT Proofs and Types - Jean-Yves Girard, Yves Lafont and Paul Taylor - 1987-90 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 (pdf)
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 Martin-Lö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
A Tutorial Implementation of a Dependently Typed Lambda Calculus - Andres Löh, Conor McBride and Wouter Swierstra wwwpdf, was previously published as "Simply Easy" pdf
The Garbage Collection Handbook, The Art of Automatic Memory Management - 2011 - Richard Jones, Antony Hosking, Eliot Moss - www
Papers
Lambda: The Ultimate GOTO - Debunking the 'Expensive Procedure Call' Myth, or, Procedure Call Implementations Considered Harmful, or, Lambda: The Ultimate GOTO - 1977 - Guy Lewis Steele, Jr. pdf
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