Programming Language Theory
Learning about Programming Language Theory can be a tough journey,
particularly for programming practitioners who haven’t studied it formally.
This resource is here to help. Please feel free to get in touch if you have
ideas for improvement.
💡 Top Tips
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 .
See also Daniel Gratzer’s Learn Type Theory, and Darryl McAdams’s So you want to learn type theory.
Type Theory
Books
- PLFA - Programming Language Foundations in Agda - Philip Wadler, Wen Kokke
- SF - Software Foundations - Benjamin C. Pierce et al. Available with jsCoq
- 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
- 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 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 (1990) and Commentary on Standard ML (1991) definition (pdf) commentary (pdf)
- The Definition of Standard ML (Revised) - Milner, Fofte, Harper, and MacQueen
- Programs and Proofs — Ilya Sergey pdf
- Type Theory and Formal Proof: An Introduction — Rob Nederpelt, Herman Geuvers
- Lectures on the Curry-Howard Isomorphism (pdf)
- Program = Proof — Samuel Mimram pdf
Papers
Videos
- OPLSS — Oregon Programming Language Summer School
- OPLSS 2023 — Types, Semantics, and Logic
- OPLSS 2022 — Types, Semantics, and Program Reasoning
- OPLSS 2021 — Foundations of Programming and Security
- 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
- Complete archives 2002-Present
- HoTTEST — Homotopy Type Theory Summer School 2022
- ICFP 2012 Monday keynote. Conor McBride: Agda-curious?
Subtopics
Programming Languages
Books
- DCPL - Design Concepts in Programming Languages – Franklyn Turbak and David Gifford, 2008. Course
- 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 - Programming Languages: Application and Interpretation - Shriram Krishnamurthi
- PAIP Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp - Peter Norvig, 1992
- PLP Programming Language Pragmatics - Michael L. Scott
- FSPL The Formal Semantics of Programming Languages - Glynn Winskel
- PL:BPC Programming Languages: Build, Prove, and Compare - Norman Ramsey
Papers
Compiler Construction
Books
- 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
- 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 phd-thesis in pdf paperback@booko More purely functional data structures
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. pdf course
- 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
- 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. The free PDF version was created by Igal Tabachnik. Video lectures based on this material: part 1, part 2, part 3.
- CT4P Category Theory for Programming — Benedikt Ahrens, Kobe Wullaert
Journals
- TAC - Theory and Applications of Categories
Subtopics
Mathematics
Some related maths resources.
Mathematical Literacy/Thinking
It can be useful to have some background in mathematical thinking.
Algebra
Other collections