Danil Annenkov's page

Photo

Currently, I am a postdoc at Aarhus University working on verification of smart contracts with Bas Spitters

Contacts

Address: IT-byen Katrinebjerg
Åbogade 34, Nygaard Building (5335), office 390,
8200 Aarhus

Email: danil.v.annenkov at gmail.com

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

Research interests

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.

Publications

Programming languages, type theory and proof assistants

Model-Driven development, software generation

Stochastic models in finance

Selected talks

Activities

Previous affiliations

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.

CV

My CV in PDF format is available here