POPL 2020 (series) / CPP 2020 (series) / The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs /
ConCert: A Smart Contract Certification Framework in Coq
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 formalization of smart contract execution in blockchains.
Slides (cpp20-ConCert-slides.pdf) | 471KiB |
Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change
Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change
10:30 - 11:35 | |||
10:30 21mTalk | Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP DOI Pre-print Media Attached | ||
10:51 21mTalk | A Mechanized Formalization of GraphQL CPP Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile DOI Pre-print Media Attached File Attached | ||
11:13 21mTalk | ConCert: A Smart Contract Certification Framework in Coq CPP Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached |