9 citations · 9 across the 2 of their papers we have counts for
4 papers
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.…
Smart Contract Interactions in Coq
Jakob Botsch Nielsen, Bas Spitters
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing…
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…