Extracting smart contracts tested and verified in Coq

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. Extracting smart contracts tested and verified in Coq. In Catalin Hritcu, Andrei Popescu 0001, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021. pages 105-121, ACM, 2021. [doi]

@inproceedings{AnnenkovMNS21,
  title = {Extracting smart contracts tested and verified in Coq},
  author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters},
  year = {2021},
  doi = {10.1145/3437992.3439934},
  url = {https://doi.org/10.1145/3437992.3439934},
  researchr = {https://researchr.org/publication/AnnenkovMNS21},
  cites = {0},
  citedby = {0},
  pages = {105-121},
  booktitle = {CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
  editor = {Catalin Hritcu and Andrei Popescu 0001},
  publisher = {ACM},
  isbn = {978-1-4503-8299-1},
}