ConCert: A smart contract certification framework in Coq

Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

31 Citationer (Scopus)

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
TitelProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA
Antal sider14
UdgivelsesstedNew York
ForlagAssociation for Computing Machinery
Publikationsdato2020
Sider215-228
ISBN (Trykt)978-1-4503-7097-4
DOI
StatusUdgivet - 2020
Begivenhed9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, USA
Varighed: 20 jan. 202021 jan. 2020

Konference

Konference9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
Land/OmrådeUSA
ByNew Orleans
Periode20/01/202021/01/2020

Fingeraftryk

Dyk ned i forskningsemnerne om 'ConCert: A smart contract certification framework in Coq'. Sammen danner de et unikt fingeraftryk.

Citationsformater