| CARVIEW |
Select Language
HTTP/2 200
last-modified: Mon, 10 Nov 2025 14:13:59 GMT
etag: "5f3e-6433e247adcc5-gzip"
accept-ranges: bytes
vary: Accept-Encoding
content-encoding: gzip
content-length: 7183
content-type: text/html
date: Sat, 27 Dec 2025 15:11:55 GMT
server: Apache / ZoneOS
Denis Firsov | Homepage
Last update: Feb 2025.
Denis Firsov
For my PhD, I studied under the
supervision of Tarmo
Uustalu at the Institute of
Cybernetics of the Tallinn
University of Technology (TUT) where I studied constructive type theory in languages like Agda and Coq.
After that, I did my postdoctoral research with Aaron Stump at
the Computational Logic
Center of the University of
Iowa where I studied impredicative type theory in Cedille language.
Then I joined R&D department
of GuardTime
where I was using EasyCrypt to derive security
of novel cryptographic constructions (digital signatures,
commitment schemes, zero-knowledge systems).
Then I held a researcher position at the Matter Labs where
we were developing Rust DSL for correct-by-construction ZK-circuits;
proving correctness of the low-level implementation of PLONK system in
EasyCrypt; and modelling system behaviour (e.g., consensus, rollups) in tools
like TLA+ and Alloy.
I currently hold a researcher position at the
Department of Software Science and a formal methods engineer position at IOG.
My Curriculum Vitae (last updated Sep. 2024).
Contact
| Email: | denis.firsov at taltech ee |
| Office: | ICT-212 |
| Address: | Akadeemia tee 15a, 12618, Tallinn, Estonia |
Research
I am interested in formally certified software, type theory, semantics of programming languages, and cryptography.Papers
-
S. Chaliasos, D. Firsov, B. Livshits Towards a Formal Foundation for Blockchain ZK Rollups.
In Proc. of the 2025 on ACM SIGSAC Conference on Computer and Communications Security, CCS '25 (Taipei, Taiwan), (to appear). doi - code & pdf -
J. B. Almeida, D. Firsov, T. Oliveira, D. Unruh Leakage-Free Probabilistic Jasmin Programs.
In Proc. of 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP '25 (Denver, CO, USA), pages 3-16. doi - code & pdf -
J. B. Almeida, D. Firsov, T. Oliveira, D. Unruh Schnorr Protocol in Jasmin.
Technical report, 2023. code & pdf -
D. Firsov, D. Unruh Zero-Knowledge in EasyCrypt.
In Proc. of 36th IEEE Computer Security Foundations Symposium, CSF '23 (Dubrovnik, Croatia), pages 226-241, 2023. doi - code & pdf -
D. Firsov, S. Laur, E. Zhuchko Unsatisfiability of Comparison-Based Non-Malleability for Commitments.
In: H. Seidl, Z. Liu, C. S. Pasareanu, eds., Proc. of 19th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2022 (Tbilisi, Sept. 2022), v. 13572 of Lect. Notes in Comput. Sci., pp. 305-323. Springer, 2022. doi - code & pdf -
D. Firsov, D. Unruh Reflection, Rewinding, and Coin-Toss in EasyCrypt.
In Proc. of 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP '22 (Philadelphia, Pennsylvania, USA), pages 166-179. doi - code & pdf -
D. Firsov, H. Lakk, S. Laur, A. Truu BLT+L: Efficient Signatures from Timestamping and Endorsements.
In Proc. of the 18th International Conference on Security and Cryptography, SECRYPT '21 (Virtual Conference), pages 75-86. doi - pdf -
D. Firsov, H. Lakk, A. Truu Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping.
In Proc. of 34th IEEE Computer Security Foundations Symposium, CSF '21 (Virtual Conference), pages 653-665. doi - code & pdf -
A. Buldas, D. Firsov, R. Laanoja, A. Truu. Verified Security of BLT Signature Scheme.
In Proc. of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP '20 (New Orleans, LA, USA). doi - code & pdf -
A. Buldas, D. Firsov, R. Laanoja, H. Lakk, A. Truu. A New Approach to Constructing Digital Signature Schemes.
In Proc. of 14th International Workshop on Security, IWSEC '19 (Tokyo, Japan, August 2019). doi - pdf -
D. Firsov, L. Diehl, C. Jenkins, A. Stump. Course-of-Value Induction in Cedille.
Manuscript, 2018. code & pdf -
L. Diehl, D. Firsov, A. Stump. Generic Zero-Cost Reuse for Dependent Types.
In Proc. of 23rd ACM SIGPLAN International Conference on Functional Programming, ICFP '18 (St. Louis, Missouri, United States, September 2018). doi - code & pdf -
D. Firsov, R. Blair, A. Stump. Efficient Mendler-Style Lambda-Encodings in Cedille.
In Proc. of 9th International Conference on Interactive Theorem Proving, ITP '18 (Oxford, July 2018). doi - code & pdf -
D. Firsov, A. Stump. Generic Derivation of Induction
for Impredicative Encodings in Cedille.
In Proc. of 7th ACM SIGPLAN Conf. on Certified Programs and Proofs, CPP '18 (Los Angeles, Jan. 2018), pp. 215-227, ACM, 2018. doi - code & pdf - D. Firsov. Certification of Context-Free Grammar Algorithms.
PhD thesis, Institute of Cybernetics at TUT, 2016. digital library - code & pdf -
D. Firsov, W. Jeltsch. Purely Functional Incremental Computing.
In F. Castor, Y. D. Liu, eds., Proc. of 20th Brazilian Symp. on Prog. Lang., SBLP 2016 (Maringá, Brazil),
v. 9889 of Lect. Notes in Comput. Sci., pp. 62-77, Springer, 2016. doi - code & pdf -
D. Firsov, T. Uustalu, N. Veltri. Variations on Noetherianness.
In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016
(Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 76-88. Open Publishing Assoc., 2016. doi - code & pdf -
D. Firsov, T. Uustalu. Dependently Typed Programming with Finite
Sets.
In Proc. of 2015 ACM SIGPLAN Wksh. on Generic Programming, WGP '15 (Vancouver, BC, Aug. 2015), ACM Press, 2015. doi - code & pdf -
D. Firsov, T. Uustalu. Certified Normalization of Context-Free
Grammars.
In Proc. of 4th ACM SIGPLAN Conf. on Certified Programs and Proofs, CPP '15 (Mumbai, Jan. 2015), ACM Press, 2015. doi - code & pdf - D. Firsov, T. Uustalu. Certified CYK Parsing of
Context-Free Languages.
J. of Log. and Algebr. Meth. in Program., v. 83, n. 5-6, pp. 459-468, 2014. doi - code & pdf - D. Firsov, T. Uustalu. Certified Parsing of Regular
Languages.
In G. Gonthier, M. Norrish, eds., Proc. of 3rd Int. Conf. on Certified Programs and Proofs, CPP 2013 (Melbourne, Dec. 2013),
v. 8307 of Lect. Notes in Comput. Sci., pp. 98-113, Springer, 2013. doi - code & pdf
Patents
- A. Truu, D. Firsov Delegated signatures for smart devices.
US Patent 11,316,698 (granted) - D. Firsov, H. Lakk Method and System for Generating Data Signatures Using an Unbounded, Stateless Private Key.
EU Patent EP4044501B1 (granted) - D. Firsov One-Time Data Signature System and Method with Untrusted Server Assistance.
US Patent App. 16/784,561 (published)
Events
| 13/10/25—17/10/25 | The 32nd ACM Conference on Computer and Communications Security (CCS), Taipei, Taiwan. Towards a Formal Foundation for Blockchain ZK Rollups. |
| 23/03/25—25/03/25 | High-Assurance Crypto Software Workshop (HACS), Sofia, Bulgaria. |
| 03/02/25—07/02/25 | EasyCrypt Retreat, Porto, Portugal. Talk: Verification of ZKPs. |
| 30/01/25—30/01/25 | Annual Seminar at Taltech, Tallinn, Estonia. Talk: Leakage-Free Probabilistic Jasmin Programs. |
| 19/01/25—25/01/25 | Certified Programs and Proofs, Denver, CO, USA. Talk: Leakage-Free Probabilistic Jasmin Programs. |
| 11/01/25—11/01/25 | World Logic Day, Tallinn, Estonia. |
| 25/11/24—30/11/24 | Agda Implementors' Meeting XXXIX, Gothenburg, Sweden. |
| 21/10/24—23/10/24 | Formal Verification of ZKP, Zurich, Switzerland. |
| 22/05/24—24/05/24 | ZKProof 6, Berlin, Germany. Talk by Ben Livshits: The Ouroboros of ZK talk |
| 23/02/24—03/03/24 | ETHDenver, Denver, USA. Talk: How do we use formal methods to harden ZK-rollups slides d/Infra Summit |
| 10/04/24—11/04/24 | ZKSummit 11, Athens, Greece. |
| 20/11/23—24/11/23 | Matter Labs offsite, Istanbul, Turkey. |
| 09/07/23—13/07/23 | 36th IEEE Computer Security Foundations Symposium, Dubrovnik, Croatia. Talk: Zero-Knowledge in EasyCrypt. slides |
| 30/03/23—01/04/23 | High-Assurance Crypto Software (HACS) meeting, Tokyo, Japan. |
| 27/02/23—10/03/23 | Workshop at Reykjavik University, Reykjavik, Iceland. Talk: EasyCrypt for working cryptographer. |
| 09/11/22—14/12/22 | Seminars at IOHK, Online. Talk: EasyCrypt for working cryptographer. slides |
| 27/09/22—30/09/22 | The 19th International Colloquium on Theoretical Aspects of Computing, Tbilisi, Georgia. Talk by Ekaterina Zhuchko: Unsatisfiability of Comparison-Based Non-Malleability for Commitments. slides |
| 17/01/22—19/01/22 | The
11th ACM SIGPLAN International Conference on Certified Programs
and Proofs, Philadelphia, Pennsylvania, USA. Talk: Reflection, Rewinding, and Coin-Toss in EasyCrypt. slides |
| 04/11/21—06/11/21 | 32nd Nordic Workshop on Programming Theory, NWPT 2021, Hybrid Conference. Talk by Ekaterina Zhuchko: Formal Analysis of Comparison-Based Non-Malleability for Commitments. extended abstract, slides |
| 09/09/21—11/09/21 | Logic and Semantics Group Outing Days. Talk: Probabilistic Reflection in EasyCrypt. |
| 21/06/21—24/06/21 | 34th IEEE Computer Security Foundations Symposium, Virtual Conference. Talk: Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping. |
| 10/06/21 | Computer Science Theory
Seminar at TUT, Tallinn, Estonia. Talk: Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping. |
| 23/02/19—24/02/19 | EUTypes meeting, Krakow, Poland. Talk: Efficient Mendler-Style Lambda-Encodings in Cedille. slides |
| 07/02/19—09/02/19 | DLT Notary Workshop, Luxembourg City, Luxembourg. |
| 23/09/18—29/09/18 | 23rd ACM SIGPLAN International Conference on Functional Programming, St. Louis, Missouri, United States. |
| 06/07/18—14/07/18 | 9th International Conference on Interactive Theorem
Proving, Oxford, UK. Talk: Efficient Mendler-Style Lambda-Encodings in Cedille. slides |
| 5/07/18 | Theory Lunch at TUT
Software Lab, Tallinn, Estonia. Talk: Generic Zero-Cost Reuse for Dependent Types. |
| 19/02/18—24/02/18 | Visiting
the Reykjavik University, Reykjavik,
Iceland. Talk: Generic Derivation of Induction for Impredicative Encodings in Cedille. |
| 07/01/18—13/01/18 | The
7th ACM SIGPLAN International Conference on Certified Programs
and Proofs, Los Angeles, CA, USA. Talk: Generic Derivation of Induction for Impredicative Encodings in Cedille. |
| 22/09/16—23/09/16 | XX
Brazilian Symposium on Programming Languages, Maringá,
Brazil. Talk: Purely functional incremental computing. |
| 21/08/16—25/08/16 | 15th
Estonian Summer School on Computer and Systems Science,
Nelijärve, Estonia. Talk: Purely functional incremental computing. |
| 26/06/16—02/07/16 | Second International Summer School on Behavioural Types, Limassol, Cyprus. |
| 01/04/16—09/04/16 | Sixth
Workshop on Mathematically Structured Functional Programming
(+ ETAPS), Eindhoven, Holland. Talk: Variations on Noetherianness. |
| 28/02/16—04/03/16 | 21st Estonian Winter School in Computer Science, Palmse, Estonia. |
| 29/01/16—31/01/16 | Theory Days at Käo, Käo, Estonia. Talk: Noetherian sets. |
| 13/11/15—15/11/15 | Estonian-Finnish logic meeting, Rakvere, Estonia. Talk: Dependently typed programming with finite sets. |
| 21/10/15—23/10/15 | 27th Nordic Workshop on Programming Theory,
Reykjavik, Iceland. Talk: Acyclic attribute evaluation in dependently typed setting, extended abstract |
| 02/10/15—04/10/15 | Theory Days at Jõeküla, Jõeküla, Estonia. |
| 18/09/15—20/09/15 | Coinduction project working meeting,
Sääritsa, Estonia. Talk: Incremental Stable Sorting in Haskell. |
| 30/08/15—05/09/15 | 11th ACM SIGPLAN Workshop on Generic Programming (+ ICFP 2015),
Vancouver, Canada. Talk: Dependently typed programming with finite sets. |
| 13/07/15—22/07/15 | Understanding Complexity and concurrency through topology of data, Camerino, Italy. |
| 06/07/15—10/07/15 | Summer School on Generic and Effectful Programming, Oxford, UK. |
| 01/03/15—06/03/15 | 20th Estonian Winter School in Computer Science, Palmse, Estonia. |
| 06/02/15—08/02/15 | Theory
Days, Rogosi, Estonia. Talk: Functional incremental computing. |
| 13/01/15—14/01/15 | The
4th ACM-SIGPLAN Conference on Certified Programs and
Proofs, Mumbai, India. Talk: Certified normalization of context-free grammars. |
| 05/12/14—06/12/14 | 8th
Annual Conference of the National Doctoral School in
Information and Communication Technologies, Rakvere,
Estonia. Talk: Functional incremental computing. |
| 10/11/14—11/11/14 | Coinduction project working meeting, Pillapalu, Estonia. |
| 02/10/14—05/10/14 | Joint Estonian-Latvian Theory Days at Ratnieki, Ratnieki, Latvia. |
| 21/09/14—23/09/14 | Coinduction Meeting, Kata, Estonia. |
| 16/05/14—18/05/14 | Theory Days, Narva-Jõesuu, Estonia. |
| 20/04/14—27/04/14 | Midlands Graduate School, Nottingham, UK. |
| 02/03/14—07/03/14 | 19th Estonian Winter School in Computer Science, Palmse, Estonia. |
| 25/10/13—27/10/13 | Theory Days, Saka, Estonia. Talk: Formalizing attribute grammars and circularity checking. |
| 17/10/13—18/10/13 | Rich Model Toolkit—Final COST Action Meeting, Madrid, Spain. Talk: Certified attribute grammar validation. |
| 08/07/13—20/07/13 | Domain specific languages summer school 2013, Cluj-Napoca, Romania. |
| 08/04/13—12/04/13 | Midlands Graduate School 2013, Leicester, England. |
| 03/03/13—08/03/13 | 18th Estonian Winter School in Computer Science, Palmse, Estonia. |
| 01/02/13—03/02/13 | Theory Days, Otepää, Estonia. Talk: Certified normalization of context-free grammars. |
| 20/01/13—21/01/13 | Workshop on Synthesis, Verification and Analysis of Rich Models, Rome, Italy. Talk: Certified normalization of context-free grammars and CYK parsing. |
| 31/10/12—02/11/12 | 24th Nordic Workshop on Programming Theory, Bergen, Norway. Talk: Certified CYK parsing of context-free languages. |
| 03/10/12—09/10/12 | The XVI edition of the Agda Implementors’ Meeting: Theory and implementation, Copenhagen, Denmark. |
| 27/09/12—30/09/12 | Joint Estonian-Latvian Theory Days at Medzābaki, Lilaste, Latvia. Talk: Certified parsing of contex-free grammars. |
| 19/08/12—23/07/12 | 11th Estonian Summer School on Computer Science, Jäneda, Estonia. |
| 16/07/12—28/07/12 | Oregon Programming Languages Summer School, Oregon, USA. |
| 26/02/12—02/03/12 | 17th Estonian Winter School in Computer Science, Palmse, Estonia. Talk: Certified parsing of regular languages. |
| 27/01/12—29/01/12 | Theory Days, Kubija, Estonia. Talk: Certified parsing. |
| 07/10/11—09/10/11 | Theory Days, Tõrve, Estonia. |
Teaching
- Logical and functional programming (Fall 2014, Fall 2013, Fall 2012, IT College).
- Functional programming (Fall 2015, IT COllege).
- Logic (Fall 2025, Taltech).
Last update: Feb 2025.