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.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA |
Antal sider | 14 |
Udgivelsessted | New York |
Forlag | Association for Computing Machinery |
Publikationsdato | 2020 |
Sider | 215-228 |
ISBN (Trykt) | 978-1-4503-7097-4 |
DOI | |
Status | Udgivet - 2020 |
Begivenhed | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, USA Varighed: 20 jan. 2020 → 21 jan. 2020 |
Konference
Konference | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 |
---|---|
Land/Område | USA |
By | New Orleans |
Periode | 20/01/2020 → 21/01/2020 |