معرفی
Denis Firsov is a researcher at the Department of Software Science at Tallinn University of Technology (TUT) and a formal methods engineer at Input Output Global (IOG). His work bridges formal methods, cryptography, and type theory, with a focus on zero-knowledge proofs, security verification, and language-based security.
He has a PhD from the Institute of Cybernetics at TUT (2016), where he studied constructive type theory using Agda and Coq. Postdoctoral research at the University of Iowa (2016-2018) involved impredicative type theory in Cedille. He has held positions at GuardTime (2018-2020) and Matter Labs (2020-2023), working on formal verification of cryptographic protocols and ZK-circuit DSLs.
Research Highlights:
- Developed formalizations for zero-knowledge protocols (Fiat-Shamir, Schnorr, Blum) in EasyCrypt
- Created Rust DSLs for ZK-circuits with formal correctness proofs
- Advanced impredicative lambda-encodings with induction in Cedille
- Contributed to parser certification for context-free and regular languages
Patents:
- US 11,316,698: Delegated signatures for smart devices
- EU EP4044501B1: Method for data signatures with unbounded keys
۰مقاله ثبتشده
