HIPERFITConCert: A Smart Contract Certification Framework in Coq
HIPERFIT Talk: “ConCert: A Smart Contract Certification Framework in Coq”
Presenter: Danil Annenkov, Post-doctorial Researcher, the Concordium Blockchain Research Center, Aarhus University
Time: Thursday, December 12, 2019, 09:30-10:15
Place: PLTC Meeting Room (HCØ-01-0-029), HCØ, Universitetsparken 5, University of Copenhagen.
Abstract:
Modern smart contract languages for blockchains tend to employ the functional programming paradigm. This fact makes them perfect targets for embedding into proof assistants allowing for convenient reasoning about their properties. But we are also interested in the meta-theory of smart contract languages and would like to have strong correctness guarantees for the embedding. We introduce ConCert: a framework allowing for both deep (AST) and shallow (Coq functions) embeddings of a smart contract language along with the soundness theorem connecting the two embeddings. The framework also features an execution model that enables reasoning about safety and temporal properties of interacting smart contracts. As an application of the developed framework, we show how to verify programs in Acorn - functional smart contract for the Concordium blockchain.
The developed techniques could be applied to the verification of programs in various (not necessarily smart contract) functional languages.
Joint work with Bas Spitters and Jakob Botsch Nielsen.
Biography
Danil Annenkov is a postdoc researcher at the Concordium Blockchain Research Center, Aarhus University working on formal verification of smart contracts. His research areas include programming language semantics, formal verification, proof assistants and type theory. Danil Annenkov received his PhD degree in Computer Science from the University of Copenhagen in 2018. After receiving his PhD degree, Annenkov was a postdoc researcher at INRIA Nantes, France, where he worked on extending the Coq proof assistant with new reasoning principles.
Host: Martin Elsman