README.md
layout  title 

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.
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
 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 – Robert Harper
 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 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 www paperback@booko
 Lambda Calculus and Combinators – J. Roger Hindley and Jonathan P. Seldin www pdf
 Semantics with Applications: An Appetizer – Hanne Riis Nielson, Flemming Nielson pdf
 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) www definition pdf commentary pdf
Papers
 Lambda Calculi with Types — Henk Barendregt pdf
 A Tutorial Implementation of a Dependently Typed Lambda Calculus – Andres Löh, Conor McBride and Wouter Swierstra www pdf, was previously published as “Simply Easy” pdf
Videos
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
Papers
 An argument against call/cc – Oleg Kiselyov www
Compiler Construction
Books
 LiSP – Lisp in Small Pieces – Christian Queinnec
 CwC Compiling with Continuations – Andrew W. Appel
 MCIiML Modern Compiler Implementation in ML – Andrew W. Appel
 pjlesterbook Implementing functional langauges: a tutorial – Simon Peyton Jones and David Lester, 1992
 slpjbook1987 – The Implementationn of Functional Programming Languages – Simon Peyton Jones – 1987
Papers
 ZINC – The ZINC experiment, an economical implementation of the ML language – Xavier Leroy (Technical Report) more OCaml papers
Videos
Runtime systems
Books
 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
 Programming in Haskell – Graham Hutton, 2007 www
 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 www
 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
 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
 Lectures on the CurryHoward Isomorphism pdf
 Purely Functional Data Structures – Chris Okasaki phdthesis in pdf paperback@booko 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, assessible, 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”.