Danil Annenkov's page

Photo

Currently, I am a postdoc at INRIA Nantes, working on CoqHoTT project with Nicolas Tabareau

Contacts

Address: LINA (main site)
UFR de Sciences et Techniques
2 rue de la Houssinière
Building 34, office 216
44300 Nantes, France

Email: danil.v.annenkov at gmail.com

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.
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.

Publications

Programming languages, type theory and proof assistants

Model-Driven development, software generation

Stochastic models in finance

Talks

Projects and repositories

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

Forcing translation in Template Coq

Implementation of the CBN forcing translation using typed meta-programing 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.

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 wider audience.

A minimal supercompiler for simple lazy language (first-order functional language) written in Stratego/XT

An interpreter and minimal supercompiler for 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 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.

CV

My CV in PDF format is available here