Programming Languages

Defines a universal computing machine and proves the undecidability of the halting problem.

The founding document of computer science. Read it once carefully; everything else is footnotes.

Basic logic, mathematical maturity

Computation has a universal model — and inherent limits no clever programming can escape.

Introduces the λ-calculus — function abstraction, application, and reduction — as a model of computation.

The conceptual ancestor of every functional language; required to read modern type-theory papers.

Basic logic

Functions and substitution are enough to express any computation.

Introduces LISP, with eval, apply, and the s-expression as both code and data.

A foundational language paper; the conceptual seed of every later language with first-class functions.

Lambda calculus, basic recursion

A small set of primitives is enough to bootstrap an entire language.

Introduces a formal logic for reasoning about program correctness with pre- and postconditions.

The foundation of program verification; you can't read modern verification papers without this.

First-order logic

You can specify what a program does separately from how it does it, and prove they match.

Models concurrency as communication between independent processes via synchronous channels.

The intellectual ancestor of Go's channels and Erlang's actor model.

Basic concurrency, first-order logic

Concurrency is communication, not shared memory.

Introduces System F (parametric polymorphism) and the underlying theory of polymorphic types.

The theoretical foundation under generics in every modern typed language.

Lambda calculus, basic type systems

Polymorphism can be a precise type-theoretic concept, not just a programming convenience.

Proves type-correctness for polymorphic functional programs and introduces type inference.

The paper that gave us ML and the entire Hindley–Milner family of inferred type systems.

System F, unification

Polymorphism plus type inference is decidable and practical.

Algorithm W — the type inference algorithm under every ML, Haskell, and Scala compiler.

The algorithmic backbone of every Hindley–Milner type system in production today.

Milner type polymorphism, unification

Type inference is a constraint-solving problem with a clean algorithmic solution.

A clean technique for proving type soundness via progress and preservation lemmas.

The default proof structure for type soundness in modern PL papers; conceptually essential.

Operational semantics, basic type theory

Type soundness is two lemmas: well-typed programs don't get stuck and types are preserved.

Shows how the category-theoretic notion of monad gives a clean handle on side effects in pure languages.

The conceptual unlock for I/O, state, and exceptions in pure functional languages.

Lambda calculus, basic Haskell helpful

Side effects can be threaded through pure code as values of a parameterised type.

Introduces continuation-passing style and definitional interpreters as semantic specifications.

A foundational paper for understanding programming-language semantics and continuations.

Lambda calculus, basic interpreters

You can specify a language's meaning by writing an interpreter for it in another language.

A static analysis that infers stack-like region annotations to manage memory without GC.

A conceptual ancestor of Rust's lifetimes and a beautiful application of type inference to memory.

Type theory, lambda calculus

Compile-time region annotations can replace runtime garbage collection in a typed setting.

A formal Iris-based proof of soundness for a substantial subset of Rust's type system.

The right reference for understanding why Rust's ownership system is actually sound.

Region-based memory management, separation logic

Even unsafe code can be encapsulated soundly inside a strongly-typed language.

An efficient algorithm for converting programs to SSA form using dominance frontiers.

The single most important compiler IR transformation; under every modern optimiser.

Compilers, control-flow graphs

A canonical IR where every variable is assigned once unlocks dataflow analysis at scale.

A compiler infrastructure designed for lifetime analysis and transformation, with a typed SSA IR.

The infrastructure under Clang, Rust, Swift, Julia, and most modern compilers.

SSA, basic compilers

A clean, typed, modular IR is the right substrate for an entire family of language tools.

The original catalogue of compiler optimisations: constant folding, CSE, dead code, code motion.

Older than most readers, but the optimisation taxonomy is essentially unchanged.

Basic compilers

Most "modern" compiler optimisations were already named and described in 1972.

Refinement types with logical predicates inferred via abstract interpretation.

A practical sweet spot between full dependent types and plain Hindley–Milner.

Type inference, basic logic

Predicate-rich types can be inferred automatically — and that changes who can use them.

A C compiler whose every optimisation is formally proved correct in Coq.

A landmark in formal verification; proves you can verify a real-world piece of software.

Coq, semantics, compilers

A real, optimising compiler can be proven correct from end to end.

The dependently-typed calculus and proof assistant that has formalised much of modern mathematics.

The most influential proof assistant of the last 30 years; the verification toolkit of choice.

Lambda calculus, type theory

A dependently-typed language can serve simultaneously as a logic and a programming language.

A modern dependently-typed proof assistant with a clean elaboration framework and serious automation.

The proof assistant of the future-decade; behind the formalisation of large mathematical results.

Coq, type theory

A well-designed elaborator and tactic framework can make formal mathematics genuinely productive.