9 citations · 9 across the 1 of their papers we have counts for
3 papers
cs.PL2020★ 9 cited
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen +1
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments.…
cs.PL2019
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
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 d…
cs.PL2018
Adventures in Formalisation: Financial Contracts, Modules, and Two-Level Type Theory
Danil Annenkov
We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compila…