We apply the zipper construct of Huet to prove
correct an optimiser for a simply-typed lambda
calculus with force and delay. The work here is
used as the basis for a certifying optimising
compiler for the Plutus smart contract language
on the Cardano blockchain.

The paper is an executable literate Agda script,
and its source may be found in the file

\texttt{Zippers.lagda.md}

available as an artifact associated with this paper.