30 citations · 39 across the 3 of their papers we have counts for
Showing 2019Show all
2 papers · 1 filter
cs.LO2019
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…
cs.PL2019★ 30 cited
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…