| 2025 | CCS | Towards a Formal Foundation for Blockchain ZK Rollups. | Stefanos Chaliasos, Denis Firsov, Benjamin Livshits |
| 2025 | CPP | Leakage-Free Probabilistic Jasmin Programs. | Jos Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh |
| 2022 | CPP | Reflection, rewinding, and coin-toss in EasyCrypt. | Denis Firsov, Dominique Unruh |
| 2022 | ICTAC | Unsatisfiability of Comparison-Based Non-malleability for Commitments. | Denis Firsov, Sven Laur, Ekaterina Zhuchko |
| 2021 | SECRYPT | BLT+L: Efficient Signatures from Timestamping and Endorsements. | Denis Firsov, Henri Lakk, Sven Laur, Ahto Truu |
| 2020 | CPP | Verified security of BLT signature scheme. | Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja |
| 2019 | IWSEC | A New Approach to Constructing Digital Signature Schemes - (Short Paper). | Ahto Buldas, Denis Firsov, Risto Laanoja, Henri Lakk, Ahto Truu |
| 2018 | CPP | Generic derivation of induction for impredicative encodings in Cedille. | Denis Firsov, Aaron Stump |
| 2018 | ITP | Efficient Mendler-Style Lambda-Encodings in Cedille. | Denis Firsov, Richard Blair, Aaron Stump |
| 2015 | CPP | Certified Normalization of Context-Free Grammars. | Denis Firsov, Tarmo Uustalu |
| 2015 | ICFP | Dependently typed programming with finite sets. | Denis Firsov, Tarmo Uustalu |
| 2013 | CPP | Certified Parsing of Regular Languages. | Denis Firsov, Tarmo Uustalu |