| Certified CYK parsing of context-free languages D Firsov, T Uustalu Journal of Logical and Algebraic Methods in Programming 83 (5-6), 459-468, 2014 | 23 | 2014 |
| Efficient mendler-style lambda-encodings in cedille D Firsov, R Blair, A Stump International Conference on Interactive Theorem Proving, 235-252, 2018 | 16 | 2018 |
| Generic zero-cost reuse for dependent types L Diehl, D Firsov, A Stump Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 15 | 2018 |
| Generic Derivation of Induction for Impredicative Encodings in Cedille D Firsov, A Stump Certified Programs and Proofs (CPP’18), 13, 2018 | 15 | 2018 |
| A new approach to constructing digital signature schemes A Buldas, D Firsov, R Laanoja, H Lakk, A Truu International Workshop on Security, 363-373, 2019 | 14 | 2019 |
| Certified parsing of regular languages D Firsov, T Uustalu International Conference on Certified Programs and Proofs, 98-113, 2013 | 13 | 2013 |
| Dependently typed programming with finite sets D Firsov, T Uustalu Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, 33-44, 2015 | 12 | 2015 |
| Certified normalization of context-free grammars D Firsov, T Uustalu Proceedings of the 2015 Conference on Certified Programs and Proofs, 167-174, 2015 | 12 | 2015 |
| Purely functional incremental computing D Firsov, W Jeltsch Brazilian Symposium on Programming Languages, 62-77, 2016 | 7 | 2016 |
| Verified security of BLT signature scheme D Firsov, A Buldas, A Truu, R Laanoja Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 5 | 2020 |
| Variations on Noetherianness D Firsov, T Uustalu, N Veltri Mathematically Structured Functional Programming MSFP2016 207, 13, 2016 | 5 | 2016 |
| A new approach to constructing digital signature schemes (extended paper) A Buldas, D Firsov, R Laanoja, H Lakk, A Truu Cryptology ePrint Archive, 2019 | 4 | 2019 |
| Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping D Firsov, H Lakk, A Truu 2021 IEEE 34th Computer Security Foundations Symposium (CSF), 1-13, 2021 | 2 | 2021 |
| Course-of-Value Induction in Cedille D Firsov, L Diehl, C Jenkins, A Stump arXiv preprint arXiv:1811.11961, 2018 | 2 | 2018 |
| Certification of context-free grammar algorithms D Firsov TUT Press, 2016 | 2 | 2016 |
| Delegated signatures for smart devices A Truu, D Firsov US Patent 11,316,698, 2022 | 1 | 2022 |
| One-Time Data Signature System and Method with Untrusted Server Assistance D Firsov US Patent App. 16/784,561, 2020 | 1 | 2020 |
| Reflection, rewinding, and coin-toss in EasyCrypt D Firsov, D Unruh Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | | 2022 |
| Formal Analysis of Non-Malleability for Commitments in EasyCrypt D Firsov, S Laur, E Zhuchko Cryptology ePrint Archive, 2022 | | 2022 |
| BLT+ L: Efficient Signatures from Timestamping and Endorsements. D Firsov, H Lakk, S Laur, A Truu SECRYPT, 75-86, 2021 | | 2021 |
Tarmo UustaluProfessor, Reykjavik University / Lead research scientist, Tallinn University of TechnologyVerified email at ru.is
