Follow
Danil Annenkov
Danil Annenkov
Aarhus University
Verified email at di.ku.dk - Homepage
Title
Cited by
Cited by
Year
Two-level type theory and applications
D Annenkov, P Capriotti, N Kraus, C Sattler
arXiv preprint arXiv:1705.03307, 2017
732017
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
48*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
292018
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
142021
Two-level type theory and applications
D Annenkov, P Capriotti, N Kraus, C Sattler
Mathematical Structures in Computer Science 33 (8), 688-743, 2023
102023
Certified compilation of financial contracts
D Annenkov, M Elsman
Proceedings of the 20th International Symposium on Principles and Practice …, 2018
102018
Extracting functional programs from Coq, in Coq
D Annenkov, M Milo, JB Nielsen, B Spitters
Journal of Functional Programming 32, e11, 2022
82022
Two-Level Type Theory and Applications.(2017)
D Annenkov, P Capriotti, N Kraus, C Sattler
URL: http://arxiv. org/abs/1705.03307, 2017
72017
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
72013
Formalising decentralised exchanges in Coq
EH Nielsen, D Annenkov, B Spitters
Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023
52023
Code Extraction from Coq to ML-like languages
D Annenkov, M Milo, B Spitters
ML 2021 Workshop, 2021
22021
Deep and shallow embeddings in Coq
D Annenkov, B Spitters
TYPES 2019, 2019
22019
Adventures in formalisation: financial contracts, modules, and two-level type theory
D Annenkov
arXiv preprint arXiv:1811.11317, 2018
22018
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
22012
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
12022
Extending MetaCoq Erasure: Extraction to Rust and Elm
D Annenkov, M Milo, JB Nielsen, B Spitters
The Coq Workshop 2021, 2021
12021
Verifying, testing and running smart contracts in ConCert
D Annenkov, M Milo, JB Nielsen, B Spitters
The Coq Workshop 2020, 2020
12020
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
12013
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
The system can't perform the operation now. Try again later.
Articles 1–20