Extracting smart contracts tested and verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters · 2021
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm.