The notion of zero-knowledge proof is a fascinating concept from
complexity theory with applications to cryptography, which arose
during the 1980s in the study of interactive proof systems.  Since
interactive proof systems are multi-round protocols between parties
who can also interact with the external world in various ways (such as
by flipping coins or by raising exceptions), they provide a natural
application for the theory of higher-order programming with effects.
In this talk, I will describe work-in-progress in which I am looking
at zero-knowledge from such a perspective, emphasising the special
role that HOPE techniques can play to clarify the (already excellent)
idea of structuring the meta-theory of cryptographic protocols around
"code-based game-playing".  In particular, taking Blum's (1986)
protocol for Hamiltonicity as a case study, I will argue for the
natural place of ideas from the control hierarchy and from the
algebraic view of effects (and especially Filinski's notion of monadic
reflection and reification).  Background to this talk is an
implementation of Blum's protocol in Haskell, and an ongoing (as yet
unfinished) refinement of this implementation to Agda, including the
completeness, soundness, and zero-knowledge properties.