A Proof-Producing Compiler for Blockchain Applications.

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

Browse the full ITP paper archive.