Two-level type theory and applications D Annenkov, P Capriotti, N Kraus, C Sattler Mathematical Structures in Computer Science 33 (8), 688-743, 2023 | 94 | 2023 |
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 | 66* | 2020 |
Static interpretation of higher-order modules in Futhark: Functional GPU programming in the large M Elsman, T Henriksen, D Annenkov, CE Oancea Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 30 | 2018 |
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 |
Extracting functional programs from Coq, in Coq D Annenkov, M Milo, JB Nielsen, B Spitters Journal of Functional Programming 32, e11, 2022 | 13 | 2022 |
Formalising decentralised exchanges in Coq EH Nielsen, D Annenkov, B Spitters Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 11 | 2023 |
Certified compilation of financial contracts D Annenkov, M Elsman Proceedings of the 20th International Symposium on Principles and Practice …, 2018 | 10 | 2018 |
Generation technique for Django MVC web framework using the stratego transformation language DV Annenkov, EA Cherkashin 2013 36th International Convention on Information and Communication …, 2013 | 8 | 2013 |
Two-Level Type Theory and Applications.(2017) D Annenkov, P Capriotti, N Kraus, C Sattler URL: http://arxiv. org/abs/1705.03307, 2017 | 6 | 2017 |
Code Extraction from Coq to ML-like languages D Annenkov, M Milo, B Spitters ML 2021 Workshop, 2021 | 4 | 2021 |
Finding smart contract vulnerabilities with ConCert's property-based testing framework M Milo, EH Nielsen, D Annenkov, B Spitters arXiv preprint arXiv:2208.00758, 2022 | 2 | 2022 |
Verifying, testing and running smart contracts in ConCert D Annenkov, M Milo, JB Nielsen, B Spitters The Coq Workshop 2020, 2020 | 2 | 2020 |
Deep and shallow embeddings in Coq D Annenkov, B Spitters TYPES 2019, 2019 | 2 | 2019 |
Adventures in formalisation: financial contracts, modules, and two-level type theory D Annenkov arXiv preprint arXiv:1811.11317, 2018 | 2 | 2018 |
Information Systems Framework Synthesis on the Base of a Logical Approach EA Cherkashin, VV Paramonov, RK Fedorov, IN Terehin, EI Pozdnyak, ... E-society Journal, 1, 2012 | 2 | 2012 |
Extending MetaCoq Erasure: Extraction to Rust and Elm D Annenkov, M Milo, JB Nielsen, B Spitters The Coq Workshop 2021, 2021 | 1 | 2021 |
A Document Content Logical Layer Induction on the Base of Ontologies and Processing Changes EA Cherkashin, PV Belykh, DV Annenkov, CK Paskal Procs. of International Conference on Applied Internet and Information …, 2013 | 1 | 2013 |
Two-level type theory and applications-ERRATUM D Annenkov, P Capriotti, N Kraus, C Sattler Mathematical Structures in Computer Science 34 (1), 80-80, 2024 | | 2024 |
Formalisations Using Two-Level Type Theory D Annenkov, P Capriotti, N Kraus Workshop on Homotopy Type Theory/Univalent Foundations, 2017 | | 2017 |
Towards Certified Compilation of Financial Contracts D Annenkov, M Elsman 28th Nordic Workshop on Programming Theory, 2016 | | 2016 |