Extracting smart contracts tested and verified in Coq

Autor: Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters

Publikováno v: Annenkov, D, Milo, M, Nielsen, J B & Spitters, B 2021, Extracting smart contracts tested and verified in Coq . in C Hritcu & A Popescu (eds), CPP 2021-Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 . Association for Computing Machinery, pp. 105-121, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021, Virtual, Online, Denmark, 17/01/2021 . https://doi.org/10.1145/3437992.3439934
CPP

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. We prove the pass correct wrt. a conventional call-by-value operationa

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a7f46278a420c7ae758750e8b9ac3122
https://pure.au.dk/portal/da/publications/extracting-smart-contracts-tested-and-verified-in-coq(4f516ec7-2331-4b35-8c2c-085622517949).html

ConCert: A Smart Contract Certification Framework in Coq

Autor: Danil Annenkov, Bas Spitters, Jakob Botsch Nielsen

Publikováno v: Annenkov, D, Nielsen, J B & Spitters, B 2019 ' ConCert : A Smart Contract Certification Framework in Coq ' arXiv.org . https://doi.org/10.1145/3372885.3373829
Annenkov, D, Botsch Nielsen, J & Spitters, B 2020, ConCert: A smart contract certification framework in Coq . in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA . Association for Computing Machinery, New York, CPP 2020-Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020, pp. 215-228, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020, New Orleans, United States, 20/01/2020 . https://doi.org/10.1145/3372885.3373829
CPP

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 deep embedding and provides a convenient way for reasoning about concre

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3dc498c8654db2eb779ee669807cd6e3