Theorem

Your hardware and compiler reorder your program. What, fences, and acquire/release actually guarantee.

2PL produces exactly the serializable schedules; anomalies are precisely what you buy by weakening it.

The correctness condition for concurrent objects, and how it differs from serializability (Conflict serializability and two-phase locking) and sequential...

Atomic registers cannot implement consensus for two threads; compare-and-swap does it for any number. Why your CPU has CAS.

Peterson's algorithm and Lamport's bakery. Correct mutual exclusion from plain reads and writes, and why modern hardware still breaks it (see Memory models and...

A randomized scheduler with a provable bound on both time and space, and why every modern runtime converged on it.

SAT is NP-complete (The Cook–Levin theorem) yet solvers handle millions of variables.

A named theory result sitting in the middle of every compiler backend, plus why the NP-hardness does not stop anyone. Part V's counterweight to all the type theory.

Exhaustively verifying concurrent systems by turning "always eventually" into an automaton, and the state-explosion wall.

Reasoning about programs as a proof system; loop invariants as the hard part, and why they can't be inferred in general.

Constant space, no false negatives, a tunable false-positive rate, and the exact formula for the tradeoff.

Relational algebra and relational calculus have equal expressive power. Why SQL is declarative and why a query planner can exist at all.

Adding a node should move 1/n of the keys, not all of them. One idea, and virtual nodes to fix its variance (Balls into bins and the power of two choices).

Sound approximation, made rigorous. The principled answer to the tradeoff Rice's theorem forces on you.

A polymorphic type alone tells you what the function must do. can only permute.

Interaction plus randomness lets a prover convince you of things you could never check alone.

"Well-typed programs don't go wrong", stated as the two lemmas that actually prove it. What a type system does and does not promise.

Every typable term has one most general type, and it's inferable. Why ML and Haskell need so few annotations, and why subtyping breaks it.

Programs are proofs, types are propositions, evaluation is proof simplification. The most beautiful idea in the series.

Three rules, all of computation, and recursion built from nothing. Absorbs Church–Rosser confluence: reduction order doesn't change the answer.