Denis Firsov

35 papers A* 1A 2B 7C 2Misc 1Journal 19Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
Crossing with Confidence: Formal Analysis and Model Checking of Blockchain Bridges.
IACR Cryptol. ePrint Arch.
Pyrros Chaidos, Pooya Farshim, Denis Firsov, Dimitar Jetchev, Aggelos Kiayias, Markulf Kohlweiss, Anca Nitulescu
2025 J jnl
Efficient Foreign-Field Arithmetic in PLONK.
IACR Cryptol. ePrint Arch.
Miguel Ambrona, Denis Firsov, Iñigo Querejeta-Azurmendi
2025 J jnl
Forking Lemma in EasyCrypt.
IACR Cryptol. ePrint Arch.
Denis Firsov, Jakub Janku
2025 B conf
Leakage-Free Probabilistic Jasmin Programs.
CPP
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
2025 A* conf
Towards a Formal Foundation for Blockchain ZK Rollups.
CCS
Stefanos Chaliasos, Denis Firsov, Benjamin Livshits
2024 J jnl
Clap: a Rust eDSL for PlonKish Proof Systems with a Semantics-preserving Optimizing Compiler.
CoRR
Marco Stronati, Denis Firsov, Antonio Locascio, Benjamin Livshits
2024 J jnl
The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation.
IACR Cryptol. ePrint Arch.
Denis Firsov, Benjamin Livshits
2024 J jnl
Towards a Formal Foundation for Blockchain Rollups.
CoRR
Stefanos Chaliasos, Denis Firsov, Benjamin Livshits
2023 J jnl
Leakage-Free Probabilistic Jasmin Programs.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
2023 J jnl
Schnorr protocol in Jasmin.
IACR Cryptol. ePrint Arch.
Denis Firsov, Tiago Oliveira, Dominique Unruh
2023 A conf
Zero-Knowledge in EasyCrypt.
CSF
Denis Firsov, Dominique Unruh
2022 J jnl
Formal Analysis of Non-Malleability for Commitments in EasyCrypt.
IACR Cryptol. ePrint Arch.
Denis Firsov, Sven Laur, Ekaterina Zhuchko
2022 B conf
Reflection, rewinding, and coin-toss in EasyCrypt.
CPP
Denis Firsov, Dominique Unruh
2022 C conf
Unsatisfiability of Comparison-Based Non-malleability for Commitments.
ICTAC
Denis Firsov, Sven Laur, Ekaterina Zhuchko
2022 J jnl
Zero-Knowledge in EasyCrypt.
IACR Cryptol. ePrint Arch.
Denis Firsov, Dominique Unruh
2021 C conf
BLT+L: Efficient Signatures from Timestamping and Endorsements.
SECRYPT
Denis Firsov, Henri Lakk, Sven Laur, Ahto Truu
2021 J jnl
Reflection, Rewinding, and Coin-Toss in EasyCrypt.
IACR Cryptol. ePrint Arch.
Denis Firsov, Dominique Unruh
2021 A conf
Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping.
CSF
Denis Firsov, Henri Lakk, Ahto Truu
2021 J jnl
Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping.
IACR Cryptol. ePrint Arch.
Denis Firsov, Henri Lakk, Ahto Truu
2020 J jnl
Verified Security of BLT Signature Scheme.
IACR Cryptol. ePrint Arch.
Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja
2020 B conf
Verified security of BLT signature scheme.
CPP
Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja
2019 J jnl
A New Approach to Constructing Digital Signature Schemes (Extended Paper).
IACR Cryptol. ePrint Arch.
Ahto Buldas, Denis Firsov, Risto Laanoja, Henri Lakk, Ahto Truu
2019 Misc conf
A New Approach to Constructing Digital Signature Schemes - (Short Paper).
IWSEC
Ahto Buldas, Denis Firsov, Risto Laanoja, Henri Lakk, Ahto Truu
2018 J jnl
Course-of-Value Induction in Cedille.
CoRR
Denis Firsov, Larry Diehl, Christopher Jenkins, Aaron Stump
2018 B conf
Efficient Mendler-Style Lambda-Encodings in Cedille.
ITP
Denis Firsov, Richard Blair, Aaron Stump
2018 J jnl
Efficient Mendler-Style Lambda-Encodings in Cedille.
CoRR
Denis Firsov, Richard Blair, Aaron Stump
2018 J jnl
Generic Zero-Cost Reuse for Dependent Types.
CoRR
Larry Diehl, Denis Firsov, Aaron Stump
2018 B conf
Generic derivation of induction for impredicative encodings in Cedille.
CPP
Denis Firsov, Aaron Stump
2018 J jnl
Generic zero-cost reuse for dependent types.
Proc. ACM Program. Lang.
Larry Diehl, Denis Firsov, Aaron Stump
2016 — conf
Purely Functional Incremental Computing.
SBLP
Denis Firsov, Wolfgang Jeltsch
2016 — conf
Variations on Noetherianness.
MSFP
Denis Firsov, Tarmo Uustalu, Niccolò Veltri
2015 B conf
Certified Normalization of Context-Free Grammars.
CPP
Denis Firsov, Tarmo Uustalu
2015 — conf
Dependently typed programming with finite sets.
WGP@ICFP
Denis Firsov, Tarmo Uustalu
2014 J jnl
Certified CYK parsing of context-free languages.
J. Log. Algebraic Methods Program.
Denis Firsov, Tarmo Uustalu
2013 B conf
Certified Parsing of Regular Languages.
CPP
Denis Firsov, Tarmo Uustalu