A Tale of Two Zippers
Publication date
2025-10-12
Authors
Wadler, Philip
Taylor, Ramsay
Krijnen, Jacco O.G.
Editors
Henglein, Fritz
Lawall, Julia
Palsberg, Jens
Ilya, Sergey
Advisors
Supervisors
Document Type
Part of book
Metadata
Show full item recordCollections
License
cc_by
Abstract
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 Zippers.lagda.md available as an artifact associated with this paper.
Keywords
Agda, Compilers, Formal Methods, Lambda Calculus, Optimisation, Computer Graphics and Computer-Aided Design, Computer Vision and Pattern Recognition, Computer Science (miscellaneous)
Citation
Wadler, P, Taylor, R & Krijnen, J O G 2025, A Tale of Two Zippers. in F Henglein, J Lawall, J Palsberg & S Ilya (eds), OLIVIERFEST 2025 - Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday. Association for Computing Machinery, pp. 239-250, 2025 Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday, OLIVIERFEST 2025, Singapore, Singapore, 12/10/25. https://doi.org/10.1145/3759427.3760383, conference