Skip to main content

A Tale of Two Zippers

OLIVIERFEST '25

#agda#formalmethods

We apply the zipper construct of Huet to prove correct anoptimiser for a simply-typed lambda calculus with force and delay. The work here is used as the basis for a certifyingoptimising compiler for the Plutus smart contract language on the Cardano blockchain.The paper is an executable literate Agda script, and itssource may be found in the file Zippers.lagda.md available as an artifact associated with this paper.

Full paper

View/download PDF

Related papers

Partner with research

Investing in and contributing to Input Output Research means supporting one of the most rigorous and peer-reviewed blockchain R&D efforts in the world. Our work bridges academia and industry, advancing decentralization, security and scalability while creating open knowledge that benefits the entire ecosystem. Whether through funding, collaboration, or partnership, contributors play a vital role in shaping innovations that are ethical, impactful and built to endure.