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.

• Introduction to Mathematical Thinking — Keith Devlin
• How to prove it — Daniel J. Velleman

• A Computational Introduction to Number Theory and Algebra — Victor Shroup
• Advanced Modern Algebra — Joseph J. Rotman pdf
• A Survey of Modern Algebra — Birkhoff and MacLane Scribd

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.

• 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
• Basic Simple Type Theory - J. Roger Hindley pdf 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
• Programs and Proofs - Ilya Sergey www pdf
• Lectures on the Curry-Howard Isomorphism 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
• ΠΣ: Dependent Types without the Sugar - Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury
• Lambda Calculi with Types — Henk Barendregt pdf

• OPLSS
  • OPLSS 2016 - Oregon Programming Language Summer School 2016
  • OPLSS 2015 - Oregon Programming Language Summer School 2015
  • OPLSS 2014 - Oregon Programming Language Summer School 2014
  • OPLSS 2013 - Oregon Programming Language Summer School 2013
  • OPLSS 2012 - Oregon Programming Language Summer School 2012
  • OPLSS 2011 - Oregon Programming Language Summer School 2011
  • OPLSS 2010 - Oregon Programming Language Summer School 2010
• ICFP 2012 Monday keynote. Conor McBride: Agda-curious?

• Higher Type Theory
• Module Systems

• 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
• PLAI-2nd - Programming Languages: Application and Interpretation - Shriram Krishnamurthi course with videos PLAI-1st
• PAIP Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp - Peter Norvig, 1992
• PLP Programming Language Pragmatics - Michael L. Scott

• An argument against call/cc - Oleg Kiselyov www

• MinCaml - A Crash Course for the MinCaml Compiler
• MCIiML Modern Compiler Implementation in ML - Andrew W. Appel
• pj-lester-book Implementing functional languages: a tutorial - Simon Peyton Jones and David Lester, 1992
• slpj-book-1987 - The Implementation of Functional Programming Languages - Simon Peyton Jones - 1987
• MCD-2e Modern Compiler Design, Second Edition — Dick Grune et al.
• EaC-2e 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
• List of compiler books at the GCC Wiki

• An Incremental Approach to Compiler Construction, Abdulaziz Ghuloum
• A Nanopass Framework for Compiler Education, Dipanwita Sarkar, Oscar Waddell, R. Kent Dybvig
• A Nanopass Framework for Commercial Compiler Development, Andrew W. Keep
• ZINC - The ZINC experiment, an economical implementation of the ML language - Xavier Leroy (Technical Report) more OCaml papers

• Coursera - Stanford - Compilers - Alex Aiken

• The Garbage Collection Handbook, The Art of Automatic Memory Management - 2011 - Richard Jones, Antony Hosking, Eliot Moss - www

• 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

• 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
• Purely Functional Data Structures - Chris Okasaki phd-thesis in pdf paperback@booko More purely functional data structures

• 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, book-length PhD on datatype generic programming.
• ICFP accepted papers
  • 2015, by session
  • 2014
  • 2013
  • 2012

• C9 Lectures: Dr. Erik Meijer - Functional Programming Fundamentals www
• C9 Lectures: Dr. Ralf Lämmel - Going Bananas + Advanced Functional Programming www
• Datatype-Generic Programming in Haskell - Andres Löh - slides in pdf

Philip Wadler's advice here is "read Pierce for motivation, Mac Lane for the presentation of the maths".

• Cakes, Custard and Category Theory: Easy recipes for understanding complex maths — Eugenia Cheng
• Category Theory, Steve Awodey. pdf
• 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
• CTCS-2nd Category Theory for Computing Science - Michael Barr and Charles Wells CTCS-1st
• 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

• Recursion Schemes

• Great Works in Programming Languages - Collected by Benjamin Piece
• Classic Papers in Programming Languages and Logic - Karl Crary
• PLT Texts Online - Frank Atanassow
• Functional programming books overview — Alex (Alexey) Ott
• TypeFunc, William Demeo
• Lambda the Ultimate - Ehud Lamm et al.
• Archives of Lambda the Ultimate (stale but includes "classic") - Chris Rathman
• Programming Language People - Chris Rathman
• PL Summer Schools forall - Aggelos Biboudis
• The Programming Language Zoo - Andrej Bauer