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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA |
| Number of pages | 14 |
| Place of publication | New York |
| Publisher | Association for Computing Machinery |
| Publication date | 2020 |
| Pages | 215-228 |
| ISBN (Print) | 978-1-4503-7097-4 |
| DOIs | |
| Publication status | Published - 2020 |
| Event | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States Duration: 20 Jan 2020 → 21 Jan 2020 |
Conference
| Conference | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 |
|---|---|
| Country/Territory | United States |
| City | New Orleans |
| Period | 20/01/2020 → 21/01/2020 |
Keywords
- Blockchain
- Certified programming
- Coq
- Functional programming languages
- Smart contracts
- Software correctness