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 |
---|---|
Publisher | arxiv.org |
Pages | 215-228 |
Number of pages | 14 |
ISBN (Electronic) | 9781450370974 |
DOIs | |
Publication status | Published - 2019 |
Keywords
- Blockchain
- Certified programming
- Coq
- Functional programming languages
- Smart contracts
- Software correctness