Proving program termination in the $\lambda$-calculus
This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.

Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step.
Such a quantity exists if and only if the lambda-term is normalizable (according to a chosen reduction strategy $\to$). Proof: suppose there is a function $f : \mathbf{\Lambda}(M_0) \to \mathbb{N}$ where $\mathbf{\Lambda}(M_0)$ is the set of lambda-terms $M$ such that $M_0 \to^\star M$, such that if $M \to M'$ then $f(M) \lt f(M')$. Then the length of a reduction chain from $M_0$ is bounded by $f(M_0)$ and in particular cannot be infinite, so $M_0$ is strongly normalizable. Conversely, if $M_0$ is strongly normalizable, define $f(M)$ as the length of the longest reduction starting at $M$.