---

layout: page title: Programming Language Theory

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

• A Tutorial Implementation of a Dependently Typed Lambda Calculus — Andres Löh, Conor McBride and Wouter Swierstra pdf. Previously published as Simply Easy.
• ΠΣ: Dependent Types without the Sugar - Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury
• Lambda Calculi with Types — Henk Barendregt
• Intuitionistic Type Theory
• Type Theory - Thierry Coquand

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

• [Higher Type Theory]({{site.github.url | replace: 'http://', '//'}}/higher-type-theory/)
• [Module Systems]({{site.github.url | replace: 'http://', '//'}}/module-systems/)
• [Effect Systems]({{site.github.url | replace: 'http://', '//'}}/effect-systems/)

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

• An argument against call/cc — Oleg Kiselyov

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](https://www.mic