【Author】
Annenkov, Danil; Nielsen, Jakob Botsch; Spitters, Bas
【Source】CPP '20: PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS
【Abstract】We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowd-funding contract based on a previous formalisation of smart contract execution in blockchains.
【Keywords】certified programming; software correctness; Coq; smart contracts; blockchain; functional programming languages
评论