11 citations · 20 across the 4 of their papers we have counts for
5 papers · 1 filter
Certified Compilation of Financial Contracts
Danil Annenkov, Martin Elsman
We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic…
Extracting functional programs from Coq, 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. We extend the MetaCoq erasure output language with typing information and use…
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.…
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…
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…