Two-Level Type Theory and Applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus (CoRR, 2017)

Certified Compilation of Financial Contracts. - Danil Annenkov; Martin Elsman (PPDP, 2018)

Adventures in Formalisation: Financial Contracts, Modules, and Two-Level Type Theory. - Danil Annenkov (CoRR, 2018)

Static interpretation of higher-order modules in Futhark: functional GPU programming in the large. - Martin Elsman; Troels Henriksen; Danil Annenkov; Cosmin E. Oancea (Proc. ACM Program. Lang., 2018)

Towards a Smart Contract Verification Framework in Coq. - Danil Annenkov; Bas Spitters (CoRR, 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)

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)

Formalising Decentralised Exchanges in Coq. - Eske Hoy Nielsen; Danil Annenkov; Bas Spitters (CPP, 2023)

Two-level type theory and applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2023)

Two-level type theory and applications - ERRATUM. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2024)