| ConCert: a smart contract certification framework in Coq D Annenkov, JB Nielsen, B Spitters Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 60 | 2020 |
| Extracting smart contracts tested and verified in Coq D Annenkov, M Milo, JB Nielsen, B Spitters Proceedings of the 10th ACM SIGPLAN International Conference on Certified …, 2021 | 24 | 2021 |
| Smart contract interactions in Coq JB Nielsen, B Spitters International Symposium on Formal Methods, 380-391, 2019 | 24 | 2019 |
| Extracting functional programs from Coq, in Coq D Annenkov, M Milo, JB Nielsen, B Spitters Journal of Functional Programming 32, e11, 2022 | 13 | 2022 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... Journal of the ACM (JACM), 1-76, 2024 | 10 | 2024 |
| Verifying, testing and running smart contracts in ConCert D Annenkov, M Milo, JB Nielsen, B Spitters | 2 | 2020 |
| Extending MetaCoq Erasure: Extraction to Rust and Elm D Annenkov, M Milo, JB Nielsen, B Spitters The Coq Workshop 2021, 2021 | 1 | 2021 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, J Nielsen, N Tabareau, ... Journal of the ACM 72 (1), 1-74, 2025 | | 2025 |
