Craig interpolation is the property held of many logics that for any valid implication A -> B there exists a formula I using only vocabulary common to both A and B such that A -> I and I -> B are both valid. The property is named after William Craig who formulated and proved the result for classical first-order logic in 1957.

Proof-theoretic treatments of interpolation, by their nature, offer further insights into a logic, such as characterising the complexity of interpolants. I will showcase several remarkable consequences of interpolation in the context of modal logic with fixed points, ranging from characterisatisons of expressivity using fixed points to the solution of certain decidability problems.