Danil Annenkov's page

Photo

From September 2022, I am a Senior Scientist at Concordium working on smart contract technology and formal verification.

Before Concordium, I was a postdoc at Aarhus University working on verification of smart contracts with Bas Spitters

Contacts

Email: danil.v.annenkov at gmail.com

My GitHub, Google Scholar profile, ResearchGate profile, arXiv profile, ORCID, dblp

Interests

I am an experienced software developer working comfortably with multiple programming paradigms. I am especially interested in applications of functional programming, domain-specific languages, and proof assistants to make better software.

My recent focus at Concordium is the Rust/Wasm stack for smart contracts and integration of cryptographic libraries from the Rust ecosystem (e.g. dalek cryptography and artworks) into the Concordium infrastructure. As part of the internal science team, I also participated in specifying a zero-knowledge query language used in the Concordium ID layer and the verifiable credentials framework.

I have research and development experience related to the financial domain: I studied stochastic models of financial instruments during my master’s and later, during my Phd studies, I accompanied this knowledge with a domain-specific language for financial contracts. My recent experience is related to another form of contract language: smart contracts for blockchains.

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.

See my CV for more information about my employment record

Projects and repositories

Not exhaustive list of projects I have contributed to. My repositories on GitHub.

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.

Publications

Programming languages, type theory and proof assistants

Model-Driven development, software generation

Stochastic models in finance

Selected talks

Academic activities

Previous academic affiliations

CV

My CV in PDF format is available here