I am interested in functional programming, type theory,
applications of proof assistants to mechanization
of programming language semantics and formalisation of mathematics (category theory).
My recent research includes formalisation of semantics of domain-specific languages
for finance, and a module system for a data-parallel functional programming
language in the Coq proof assistant.
During my PhD I was visiting University of Nottingham, where I worked with Paolo Capriotti and Nicolai Kraus on formalisation of two-level type theory (Homotopy Type Theory extended with strict equality) in the Lean proof assistant.
Programming languages, type theory and proof assistants
- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. “Extracting Tested and Verified Smart Contracts in Coq”. CPP'2021. To appear. [Conference website]
- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. “Verifying, testing and running smart contracts in ConCert”. Extended abstract. The Coq workshop 2020. [PDF][Coq code]
- Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters. ConCert: A Smart Contract Certification Framework in Coq. CPP'2020. [PDF][arXiv][Coq code]
- Danil Annenkov, Bas Spitters. Deep and Shallow Embeddings in Coq. TYPES-2019. [PDF]
- Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler. Two-Level Type Theory and Applications. Submitted to Mathematical Structures in Computer Science (MSCS), 2019. [arXiv] [ Lean code]
- Danil Annenkov, Martin Elsman. Certified Compilation of Financial Contracts. PPDP’18. [PDF] [ACM] [Futhark, Haskell and Coq code]
- Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin Oancea. Static Interpretation of Higher-Order Modules in Futhark: functional GPU programming in the large. ICFP’18. [PDF] [ACM OpenAccess] [Coq formalisation]
- Adventures in Formalisation: Financial Contracts, Modules, and Two-Level Type Theory. PhD thesis, University of Copenhagen, 2018 [PDF] [arXiv]
- Danil Annenkov and Martin Elsman. Towards Certified Compilation of Financial Contracts. In Proceedings of the 28th Nordic Workshop on Programming Theory (NWPT’16). Aalborg, DK. November, 2016 [PDF] [ Proceedings ] [Haskell and Coq code]
- Annenkov, D.V., Cherkashin, E.A., Generation technique for Django MVC web framework using the Stratego transformation language. 36th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), IEEE, pp. 1084-1087, 2013 [PDF] [IEEEXplore ].
- Annenkov, D.V., Domain-specific languages as a foundation of the approach to software development. Proceedings of the conference “Vinerovskie chteniya”, pp. 142-146 (in Russian), 2013.
Model-Driven development, software generation
- Evgeny A. Cherkashin , Polina V. Belykh, Danil V. Annenkov, Christina K. Paskal. A Document Content Logical Layer Induction on the Base of Ontologies and Processing Changes. Proc. of International Conference on Applied Internet and Information Technologies, University of Novi Sad Technical Faculty «Mihailo Pupin», Zrenjanin, Serbia, 2013. C. 252-257. [PDF] [ Proceedings ]
- Cherkashin, E.A., Paramonov, V.V., Fedorov, R.K., Terehin, I.N., Pozdnyak, E.I., Annenkov, D.V., Information Systems Framework Synthesis on the Base of a Logical Approach. Proceedings of International Conference on Applied Internet and Information Technologies, October 26, Serbia, Zrenjanin. pp. 239-244, 2012. [PDF] [ Proceedings ]
Stochastic models in finance
- Annenkov, D.V. Dynamics of price changes of financial instruments (some problems of theory and practice). ECONOMINFO #6, 2006. (in Russian: Анненков, Д. В. (2006). Динамика изменения цен финансовых инструментов (некоторые проблемы теории и практики). ЭКОНОМИНФО, (6)). [ PDF] [ DOI: 10.24412/Fioqh9UJ8yg]
- Annenkov, D.V., Simulation and research of the securities market. Bulletin of the Irkutsk State Technical University, vol. 27, #3, pp. 68-71 (in Russian), 2006.
- Annenkov, D.V., Petukhov, P.A., Torbeeva, A.S., Modeling the organization and functioning of the securities market. Proceedings of conference “Vinerovskie chteniya”, pp. 35-40, 2005
- Verifying, testing and running smart contracts in ConCert, The Coq Workshop (virtual), July 2020. [Slides] [Video] [Extended abstract]
- ConCert: A Smart Contract Certification Framework in Coq. Certified Programs and Proofs, New Orleans, Louisiana, United States, January 2020. [Slides] [Video]
- A lecture on smart contracts on the association of computer scientists (Datalogforeningen) meeting. Aarhus, Denmark, November 2019. [Slides]
- Deep and Shallow Embeddings in Coq. Oslo, Norway. 25th International Conference on Types for Proofs and Programs (TYPES), June 2019. [Slides]
- Towards Safer Smart Contract Languages. Digital Innovation Festival. Aarhus, Denmark, April 2019. [Slides]
- Nominal Techniques in Coq. HIPERFIT Workshop 2018. [Slides] [Coq code]
- Danil Annenkov (work with Paolo Capriotti and Nicolai Kraus). Formalisations Using Two-Level Type Theory. HoTT/UF Workshop 2017, Oxford, UK. [Slides] [Abstract]
- Towards Certified Compilation of Financial Contracts. Nordic Workshop on Programming Theory(NWPT’16), November 2016. [Slides]
- Verifying the generation of payoff-language expressions. HIPERFIT Workshop, March 2016 [Slides]
Projects and repositories
Implementation of the CBN forcing translation using typed meta-programming facilities of Template Coq. Based on the OCaml forcing translation plugin (by Jaber, Pédrot, Sozeau, Lewertowski and Tabareau, link to the repo ). Current implementation uses the version of Coq supporting definitional proof-irrelevance (by Gaëtan Gilbert, link to the repo ).
An implementation of two-level type theory in the Lean proof assistant. Two-level type theory is a version of Martin-Löf type theory (MLTT), which consists of two fragments: the fibrant fragment (Homotopy Type Theory) and the strict fragment (MLTT with uniqueness of identity proofs). In our development in the Lean proof assistant we demonstrate, how two-level type theory can be encoded in existing proof assistant. Using the definition of category from Lean's standard library, we define limits and construct general limits in the category of pretypes in the strict fragment. Also, we define inverse diagrams and show how some results of the theory of inverse diagrams can be internalised in two-level type theory and developed in the proof assistant.
An extension of the Contract DSL presented in ICFP 2015 paper with templating features, and certified compilation to a simple intermediate payoff expression language (PEL). This expression language can be used to obtain so called "payoff expression" for using in a context of a "pricing engine" (software, that uses probabilistic modeling of possible future contract price using Monte-Carlo simulation). We use Coq to prove soundness of the compiler from the Contract DSL to PEL, and use Coq's code extraction feature, to obtain correct Haskell implementation of the compiler.
An elegant and self-contained proof of normalisation for call-by-value simply-typed lambda calculus using Tait's method in the Coq proof assistant. Nominal representation of variables. Categorical semantics of the simply-typed lambda calculus.
Haskell implementation of a simple contract management system, where contracts are represented using the Contract DSL. The prototype features web-interface with automatically generated input forms from Haskell data type definitions, and integration with FINPAR (high-performance pricing engine) through OpenCL code generation.
A simple program specializer (based on partial evaluation) for a subset of Scheme, originally developed by Sergei Romanenko in 1990-1993, ported to the modern scheme-like Racket language to make UNMIX usable for a wider audience.
A minimal supercompiler for simple lazy language (first-order functional language) written in Stratego/XT
An interpreter and a minimal supercompiler for SLL (Simple Lazy Language - first-order functional language) written in Stratego/XT transformation language, part of the Spoofax language workbench. Minimal supercompiler implementation is inspired by the elegant Haskell implementation SC Mini. Spoofax works on Eclipse platform and allows one to create a full-featured IDE plugin with syntax highlighting, perform semantic analysis and context completion. My implementation aims to give an environment to experiment with the supercompiler for educational purposes.
Implementation of brute-force Regulatory Motifs Finding algorithm (formulated as a median string problem) with two branch-and-bound strategies.