Danil Annenkov

Registered user since Fri 13 Dec 2019

Name:Danil Annenkov

Danil Annenkov is a postdoc researcher at the Concordium Blockchain Research Center, Aarhus University working on formal verification of smart contracts. His research areas include programming language semantics, formal verification, proof assistants and type theory. Danil Annenkov received his PhD degree in Computer Science from the University of Copenhagen in 2018 under the supervision of Martin Elsman. After receiving his PhD degree, Annenkov was a postdoc researcher at INRIA Nantes, France, where he worked on extending the Coq proof assistant with new reasoning principles.

Affiliation:Concordium Blockchain Research Center, Aarhus University
Personal website:http://dannenkov.me
Research interests:type theory, proof assistants, programming language semantics, functional programming


ML 2021 Author of Code Extraction from Coq to ML-like languages within the ML 2021-track
CPP 2021 Author of Extracting Smart Contracts Tested and Verified in Coq within the CPP 2021-track
CPP 2020 Author of ConCert: A Smart Contract Certification Framework in Coq within the CPP 2020-track