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

Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework. - Mikkel Milo; Eske Hoy Nielsen; Danil Annenkov; Bas Spitters (FMBC@CAV, 2022)

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