My student Peng (Frank) Fu has recently written up a short note (3 pages) with a reducibility proof for call-by-value (CBV) simply typed lambda calculus (STLC). This may be useful for those interested in how one shows termination of STLC by the reducibility method. Note that simpler methods exist for showing certainly at least (weak) normalization of STLC, but reducibility is a very useful tool for analyzing stronger systems. Peng’s note is based on a short note (4 pages) I wrote up for one of my classes, showing strong normalization for STLC with full beta-reduction. The restriction to CBV simplifies the proof, although it requires ensuring explicitly that terms are closed (have no free variables). For the CBV case, a similar proof is given in Chapter 12 of Benjamin Pierce’s Types and Programming Languages book. The main differences between Frank’s proof and the one in Chapter 12 of Pierce are that: (1) reducible terms are not assumed to be typable, and (2) an inductive definition is given for the substitutions which replace variables by reducible terms (simplifying the notation somewhat).