ConCert: A Smart Contract Certification Framework in Coq

Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters

Publikation: Working paper/Preprint Working paperForskningpeer review

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 crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.
OriginalsprogEngelsk
Udgiverarxiv.org
Sider215-228
Antal sider14
ISBN (Elektronisk)9781450370974
DOI
StatusUdgivet - 20 jan. 2020

Fingeraftryk

Dyk ned i forskningsemnerne om 'ConCert: A Smart Contract Certification Framework in Coq'. Sammen danner de et unikt fingeraftryk.

Citationsformater