Wadler's Blog: Smaller, cheaper Plutus scripts with the UPLC command-line tool

Philip Wadler points to a blog post by colleague Ziyang Liu at Input Output about the UPLC command-line tool, which produces smaller and cheaper Plutus scripts. The tool uses Agda to provide certificates validating the correctness of compiler passes. A simplified description of one such pass is covered in the paper 'A Tale of Two Zippers' by Wadler, Krijnen, and Taylor.