Smart Contract Interactions in Coq. - Jakob Botsch Nielsen; Bas Spitters (FM Workshops (1), 2019)

ConCert: a smart contract certification framework in Coq. - Danil Annenkov; Jakob Botsch Nielsen; Bas Spitters (CPP, 2020)

Extracting smart contracts tested and verified in Coq. - Danil Annenkov; Mikkel Milo; Jakob Botsch Nielsen; Bas Spitters (CPP, 2021)

Extracting functional programs from Coq, in Coq. - Danil Annenkov; Mikkel Milo; Jakob Botsch Nielsen; Bas Spitters (J. Funct. Program., 2022)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 2025)