The notion of “zero-knowledge proof” (an instance of the more general notion of “interactive proof”) is an intriguing concept from cryptography and complexity theory, originating in the 1980s. The intuitive idea is that by following a zero-knowledge protocol, one party (“the prover”) manages to convince another party (“the verifier”) of the truth of some proposition (e.g., that a particular graph contains a Hamiltonian cycle), but without revealing any of its secret knowledge for why the proposition is true (e.g., here, the verifier learns nothing about the actual Hamiltonian cycle, other than that it exists).

In this INFORMAL TALK, I will begin by recalling the formal definitions of interactive proof and of zero-knowledge, and then describe some of my ongoing work trying to better understand these concepts from the perspective of constructive logic and type theory. Zero-knowledge seems to represent a paradox to the pure constructivist (what does it mean to prove an existential statement without also showing how to build an object?), and my goal is to try to resolve this paradox by taking a broader view of constructive logic, in particular including the important notions of continuations and side-effects. After the initial introduction, the talk will consist of an interactive walk-through of some Haskell code.