wadler.blogspot.com·há 3 meses Smaller, cheaper Plutus scripts with the UPLC command-line tool
If you want to see a use of Agda in real life, to provide certificates validating the correctness of compiler passes, check out this blog post from my colleague Ziyang Liu at Input Output. A simplifie
