ConCert: A Smart Contract Certification Framework in Coq

TY - UNPB

T1 - ConCert

T2 - A Smart Contract Certification Framework in Coq

AU - Annenkov, Danil

AU - Nielsen, Jakob Botsch

AU - Spitters, Bas

PY - 2019

Y1 - 2019

N2 - 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 crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.

AB - 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 crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.

KW - Blockchain

KW - Certified programming

KW - Coq

KW - Functional programming languages

KW - Smart contracts

KW - Software correctness

UR - http://www.scopus.com/inward/record.url?scp=85079467423&partnerID=8YFLogxK

U2 - 10.1145/3372885.3373829

DO - 10.1145/3372885.3373829

M3 - Working paper

SP - 215

EP - 228

BT - ConCert

PB - arxiv.org

ER -