ConCert: A smart contract certification framework in Coq

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

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.

Original languageEnglish
Title of host publicationProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA
Number of pages14
Place of publicationNew York
PublisherAssociation for Computing Machinery
Publication year2020
Pages215-228
ISBN (print)978-1-4503-7097-4
DOIs
Publication statusPublished - 2020
Event9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States
Duration: 20 Jan 202021 Jan 2020

Conference

Conference9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
LandUnited States
ByNew Orleans
Periode20/01/202021/01/2020
SponsorACM SIGPLAN
SeriesCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020

    Research areas

  • Blockchain, Certified programming, Coq, Functional programming languages, Smart contracts, Software correctness

See relations at Aarhus University Citationformats

ID: 181347291