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.
I did my PhD at the University of Copenhagen under the supervision of Martin Elsman. 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.
I spent a year at INRIA Nantes working with Nicolas Tabareau on formalising the forcing translation in MetaCoq.
Programming languages, type theory and proof assistants
- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. "Extracting functional programs from Coq, in Coq". Accepted to Journal of Functional Programming (JFP). 2022. [PDF] [arXiv]
- Danil Annenkov, Mikkel Milo, and Bas Spitters. "Code Extraction from Coq to ML-like languages". Extended abstract. ML Workshop 2021. [PDF]
- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. "Extending MetaCoq Erasure: Extraction to Rust and Elm". Extended abstract. The Coq Workshop 2021. [PDF] [Workshop program] [Slides]
- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. “Extracting Tested and Verified Smart Contracts in Coq”. CPP'2021. [PDF] [arXiv] [DOI: 10.1145/3437992.3439934] [Coq code]
- 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] [DOI: 10.1145/3236950.3236955] [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
- Smart contracts in a proof assistant, The COBRA seminar (Aarhus University), October 2021. [Slides]
- Extracting Tested and Verified Smart Contracts in Coq, CPP'2021 (Denmark, virtual), January 2021. [Slides] [Long video] [Short video]
- 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]
- Formalisations Using Two-Level Type Theory (with Paolo Capriotti and Nicolai Kraus), 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]
- Spring 2021. PC member of Software Engineering and Information Management (SEIM’21) conference.
- Fall 2019 - spring 2021. Organising the LogSem seminar at Aarhus University, Logic and Semantics group.
- Feb. 2018 - Nov. 2018. Postdoc at INRIA Nantes, working on CoqHoTT project with Nicolas Tabareau
- Nov. 2014 - Jan. 2018. PhD student at University Of Copenhagen on HIPERFIT project under the supervision of Martin Elsman
Projects and repositories
Not exhaustive list of projects I have contributed to. My repositories: on GitHub, on Bitbucket
Trace monoids in Cubical Agda
A definition of the trace monoid (free partially commutative monoid) using HITs. Some simple examples, including reasoning about database transaction schedules.
Forcing translation in Template Coq
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 ).
Two-level type theory
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.
Financial Contracts DSL
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.
Normalisation for Simply-Typed Lambda-calculus in Coq [nice-looking coqdoc-html version]
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.
The HIPERFIT Portfolio Management Prototype
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.
UNMIX ported to Racket
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.
Some bioinformatics algorithms in Haskell
Implementation of brute-force Regulatory Motifs Finding algorithm (formulated as a median string problem) with two branch-and-bound strategies.