معرفی
Danil Annenkov is a researcher at the Concordium Blockchain Research Center, Aarhus University. Previously, he held postdoctoral positions at Aarhus University and INRIA Nantes, France. His academic work focuses on formal verification of smart contracts, programming language semantics, proof assistants, type theory, and functional programming.
- Concordium Blockchain Research Center (Aarhus University)
- INRIA Nantes, France
- University of Copenhagen (PhD institution)
His research addresses critical areas in computer science, particularly blockchain security and formal methods. Danil's work bridges theoretical type theory with practical applications in smart contract verification and program transformation. He contributes to extending proof assistants like Coq with advanced reasoning principles.
The articles listed reflect his expertise in blockchain verification, Coq-based certification frameworks, and programming language design. His publications span conferences like CPP and ML, emphasizing formal methods in decentralized systems.
Danil has been actively involved in academic events such as CoqPL (serving as a Program Committee member) and CPP/ML tracks of POPL. His technical work includes implementing interpreters and supercompilers in Stratego transformation language for program analysis.
He contributes to open-source projects like the Stratego-based stratego-sll interpreter for first-order functional language transformation, available on GitHub. His tools facilitate research in program specialization and formal verification workflows.
