This website uses cookies to store user session information. By using our website you consent to our terms of use. Read more
I agree

Denis Firsov

https://etis.ee/CV/Denis_Firsov/eng
28.05.1987
Scopus Author Id 56016511700

Career

Institutions and positions
01.02.2019–...   
Tallinn University of Technology , School of Information Technologies, Department of Software Science, Researcher (0,20)
07.01.2019–...   
Guardtime AS, engineer (0,80)
19.01.2017–04.12.2018   
The University of Iowa, Post-Doc (1,00)
01.12.2015–18.01.2017   
Tallinn University of Technology , Institute of Cybernetics at TUT, Junior Researcher (1,00)
01.06.2011–30.11.2015   
Tallinn University of Technology , Institute of Cybernetics at TUT, engineer (1,00)
 
 
Education
2012–31.08.2016   
Tallinn University of Technology, PhD studies in information and communication technology
2010–2012   
Tallinn University of Technology, master's studies in informatics
2006–2010   
Estonian Information Technology College, professional higher education studies in IT systems development

Qualifications

Academic degrees
Denis Firsov, Doctor's Degree, 2016, (sup) Tarmo Uustalu, Certification of context-free grammar algorithms, Tallinn University of Technology Institute of Cybernetics at TUT.
Denis Firsov, Master's Degree, 2012, (sup) Tarmo Uustalu, Certified parsing of regular languages, Tallinn University of Technology Institute of Cybernetics at TUT.
 
 
Fields of research
ETIS CLASSIFICATION: 4. Natural Sciences and Engineering; 4.6. Computer Sciences; CERCS CLASSIFICATION: P170 Computer science, numerical analysis, systems, control
 
 

Projects in progress

Completed projects

Publications

Category
Year
Publication
 
3.1.
2020
Firsov, Denis; Buldas, Ahto; Truu, Ahto; Laanoja, Risto (2020). Verified security of BLT signature scheme. CPP '20 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs : January 20-21, 2020, New Orleans, LA, US. Ed. Blanchette, Jasmin; Hriţcu, Cătălin. New York, NY: ACM, 244−257. DOI: 10.1145/3372885.3373828.
3.1.
2019
Buldas, Ahto; Firsov, Denis; Laanoja, Risto; Lakk, Henri; Truu, Ahto (2019). A new approach to constructing digital signature schemes : (short paper). Advances in Information and Computer Security : 14th International Workshop on Security, IWSEC 2019, Tokyo, Japan, August 28-30, 2019, Proceedings. Ed. Attrapadung, Nuttapong; Yagi, Takeshi. Cham: Springer, 363−373. (Lecture Notes in Computer Science; 11689).10.1007/978-3-030-26834-3_21.
1.2.
2018
Diehl, Larry; Firsov, Denis; Stump, Aaron (2018). Generic zero-cost reuse for dependent types. Proceedings of the ACM on Programming Languages, 2 (ICFP), article 104. DOI: 10.1145/3236799.
3.1.
2018
Firsov, Denis; Stump, Aaron (2018). Generic derivation of induction for impredicative encodings in Cedille. CPP '18: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 8–9, 2018 Los Angeles, CA, USA. Ed. Andronick, June; Felty, Amy. New York: ACM, 215−227.10.1145/3167087.
3.1.
2018
Firsov, Denis; Blair, Richard; Stump, Aaron (2018). Efficient Mendler-style lambda-encodings in Cedille. Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FLoC 2018, Oxford, UK, July 9-12, 2018, Proceedings, 10895. Ed. Avigad, Jeremy; Mahboubi, Assia. Cham: Springer, 235−252. (Lecture Notes in Computer Science).10.1007/978-3-319-94821-8_14.
2.3.
2016
Firsov, Denis (2016). Certification of context-free grammar algorithms. (Doktoritöö, Tallinn University of Technology, Institute of Cybernetics). Tallinn: TUT Press.
3.1.
2016
Firsov, Denis; Jeltsch, Wolfgang (2016). Purely functional incremental computing. Programming Languages : 20th Brazilian Symposium, SBLP 2016, Maringá, Paraná, Brazil, September 19-23, 2016. Ed. Castor, Fernando; Liu, Yu David. Berlin: Springer, 62−77. (Lecture Notes in Computer Science; 9889).10.1007/978-3-319-45279-1_5.
3.1.
2016
Firsov, Denis; Uustalu, Tarmo; Veltri, Niccolò (2016). Variations on Noetherianness. Proceedings 6th Workshop on Mathematically Structured Functional Programming (MSFP 2016) : Eindhoven, The Netherlands, 8 April 2016. Ed. Atkey, Robert; Krishnaswami, Neel. Sydney: Open Publishing Association, 76−88. (Electronic Proceedings in Theoretical Computer Science; 207). DOI: 10.4204/eptcs.207.4.
5.2.
2016
Firsov, Denis (2016). Certified algorithms for context-free grammars [PhD abstracts / Graham Hutton]. Journal of Functional Programming, 26, e24, 12 −13.
3.1.
2015
Firsov, Denis; Uustalu, Tarmo (2015). Dependently typed programming with finite sets. WGP '15 : Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, August 30, 2015, Vancouver, BC, Canada. New York: ACM, 33−44. DOI: 10.1145/2808098.2808102.
3.1.
2015
Firsov, Denis; Uustalu, Tarmo (2015). Certified normalization of context-free grammars. CPP '15 : Proceedings of the 2015 ACM Conference on Certified Programs and Proofs, January 13-14, 2015, Mumbai, India. New York: ACM, 167−174. DOI: 10.1145/2676724.2693177.
1.1.
2014
Firsov, Denis; Uustalu, Tarmo (2014). Certified CYK parsing of context-free languages. Journal of Logical and Algebraic Methods in Programming, 83, 459−468. DOI: 10.1016/j.jlamp.2014.09.002.
3.1.
2013
Firsov, Denis; Uustalu, Tarmo (2013). Certified parsing of regular languages. Certified Programs and Proofs : Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Ed. Gonthier, Georges; Norrish, Michael. Cham: Springer, 98−113. (Lecture Notes in Computer Science; 8307).
2.3.
2012
Firsov, Denis (2012). Certified parsing of regular languages. (Magistritöö, Tallinn University of Technology, Institute of Cybernetics). Tallinn: Institute of Cybernetics at Tallinn University of Technology.

Industrial property

29.10.2020

Denis Firsov

https://etis.ee/CV/Denis_Firsov/est
28.05.1987
http://firsov.ee/
Scopus Author Id 56016511700

Teenistuskäik

Töökohad ja ametid
01.02.2019–...   
Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut, Teadur (0,20)
07.01.2019–...   
Guardtime AS, insener (0,80)
19.01.2017–04.12.2018   
Iowa Ülikool, Järeldoktor (1,00)
01.12.2015–18.01.2017   
Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut, Nooremteadur (1,00)
01.06.2011–30.11.2015   
Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut, insener (1,00)
 
 
Haridustee
2012–31.08.2016   
Tallinna Tehnikaülikool, doktorantuur info- ja kommunikatsioonitehnoloogias
2010–2012   
Tallinna Tehnikaülikool, magistriõpingud informaatikas
2006–2010   
Eesti Infotehnoloogia Kolledž, rakenduskõrgharidusõpingud IT süsteemide arenduses

Kvalifikatsioon

Teaduskraadid
Denis Firsov, Doctor's Degree, 2016, (sup) Tarmo Uustalu, Certification of context-free grammar algorithms, Tallinn University of Technology Institute of Cybernetics at TUT.
Denis Firsov, Master's Degree, 2012, (sup) Tarmo Uustalu, Certified parsing of regular languages, Tallinn University of Technology Institute of Cybernetics at TUT.
 
 
Teadustöö põhisuunad
ETIS KLASSIFIKAATOR: 4. Loodusteadused ja tehnika; 4.6. Arvutiteadused; CERCS KLASSIFIKAATOR: P170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)

Jooksvad projektid

Lõppenud projektid

Publikatsioonid

Klass
Aasta
Publikatsioon
 
3.1.
2020
Firsov, Denis; Buldas, Ahto; Truu, Ahto; Laanoja, Risto (2020). Verified security of BLT signature scheme. CPP '20 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs : January 20-21, 2020, New Orleans, LA, US. Ed. Blanchette, Jasmin; Hriţcu, Cătălin. New York, NY: ACM, 244−257. DOI: 10.1145/3372885.3373828.
3.1.
2019
Buldas, Ahto; Firsov, Denis; Laanoja, Risto; Lakk, Henri; Truu, Ahto (2019). A new approach to constructing digital signature schemes : (short paper). Advances in Information and Computer Security : 14th International Workshop on Security, IWSEC 2019, Tokyo, Japan, August 28-30, 2019, Proceedings. Ed. Attrapadung, Nuttapong; Yagi, Takeshi. Cham: Springer, 363−373. (Lecture Notes in Computer Science; 11689).10.1007/978-3-030-26834-3_21.
1.2.
2018
Diehl, Larry; Firsov, Denis; Stump, Aaron (2018). Generic zero-cost reuse for dependent types. Proceedings of the ACM on Programming Languages, 2 (ICFP), article 104. DOI: 10.1145/3236799.
3.1.
2018
Firsov, Denis; Stump, Aaron (2018). Generic derivation of induction for impredicative encodings in Cedille. CPP '18: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 8–9, 2018 Los Angeles, CA, USA. Ed. Andronick, June; Felty, Amy. New York: ACM, 215−227.10.1145/3167087.
3.1.
2018
Firsov, Denis; Blair, Richard; Stump, Aaron (2018). Efficient Mendler-style lambda-encodings in Cedille. Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FLoC 2018, Oxford, UK, July 9-12, 2018, Proceedings, 10895. Ed. Avigad, Jeremy; Mahboubi, Assia. Cham: Springer, 235−252. (Lecture Notes in Computer Science).10.1007/978-3-319-94821-8_14.
2.3.
2016
Firsov, Denis (2016). Certification of context-free grammar algorithms. (Doktoritöö, Tallinn University of Technology, Institute of Cybernetics). Tallinn: TUT Press.
3.1.
2016
Firsov, Denis; Jeltsch, Wolfgang (2016). Purely functional incremental computing. Programming Languages : 20th Brazilian Symposium, SBLP 2016, Maringá, Paraná, Brazil, September 19-23, 2016. Ed. Castor, Fernando; Liu, Yu David. Berlin: Springer, 62−77. (Lecture Notes in Computer Science; 9889).10.1007/978-3-319-45279-1_5.
3.1.
2016
Firsov, Denis; Uustalu, Tarmo; Veltri, Niccolò (2016). Variations on Noetherianness. Proceedings 6th Workshop on Mathematically Structured Functional Programming (MSFP 2016) : Eindhoven, The Netherlands, 8 April 2016. Ed. Atkey, Robert; Krishnaswami, Neel. Sydney: Open Publishing Association, 76−88. (Electronic Proceedings in Theoretical Computer Science; 207). DOI: 10.4204/eptcs.207.4.
5.2.
2016
Firsov, Denis (2016). Certified algorithms for context-free grammars [PhD abstracts / Graham Hutton]. Journal of Functional Programming, 26, e24, 12 −13.
3.1.
2015
Firsov, Denis; Uustalu, Tarmo (2015). Dependently typed programming with finite sets. WGP '15 : Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, August 30, 2015, Vancouver, BC, Canada. New York: ACM, 33−44. DOI: 10.1145/2808098.2808102.
3.1.
2015
Firsov, Denis; Uustalu, Tarmo (2015). Certified normalization of context-free grammars. CPP '15 : Proceedings of the 2015 ACM Conference on Certified Programs and Proofs, January 13-14, 2015, Mumbai, India. New York: ACM, 167−174. DOI: 10.1145/2676724.2693177.
1.1.
2014
Firsov, Denis; Uustalu, Tarmo (2014). Certified CYK parsing of context-free languages. Journal of Logical and Algebraic Methods in Programming, 83, 459−468. DOI: 10.1016/j.jlamp.2014.09.002.
3.1.
2013
Firsov, Denis; Uustalu, Tarmo (2013). Certified parsing of regular languages. Certified Programs and Proofs : Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Ed. Gonthier, Georges; Norrish, Michael. Cham: Springer, 98−113. (Lecture Notes in Computer Science; 8307).
2.3.
2012
Firsov, Denis (2012). Certified parsing of regular languages. (Magistritöö, Tallinn University of Technology, Institute of Cybernetics). Tallinn: Institute of Cybernetics at Tallinn University of Technology.

Tööstusomand

29.10.2020

Search project

  • {{item.Name}}
Institution is projects' financier   Institution is projects' executor  
  • {{searchListItem.Name}}
All   Projects   Master projects   Subprojects  
New Frascati (2015)
Old and new Frascati
All
Ongoing
Finished
Beginning
Fuzzy
Precise
Simple Search Clear
  • Found 7 results
ProgramTypeNumberNameProject startProject endPrincipal investigatorInstitutionFinancing
TKEXCSEstonian Excellence in Computer Science - EXCS07.07.200831.08.2015Tarmo UustaluTallinn University of Technology ; Tallinn University of Technology , Institute of Cybernetics at TUT4 244 372,58 EUR
MUUIKT29 (3.2.1201.13-0029)Coinduction for semantics, analysis and verification of communicating and concurrent reactive software01.03.201330.11.2015Tarmo UustaluTallinn University of Technology , Institute of Cybernetics at TUT526 194,00 EUR
1.1.3.EITSA18017Research measure of IT Academy programme for 2018-2022: Software trustworthiness01.01.201831.12.2022Paweł Maria SobocińskiTallinn University of Technology , School of Information Technologies, Department of Software Science1 864 416,00 EUR
TKSubprojectTAR16013 (EXCITE) (TK148)Estonian Centre of Excellence in ICT Research01.09.201601.03.2023Maarja KruusmaaTallinn University of Technology , School of Information Technologies, Centre for Biorobotics; Cybernetica AS2 121 014,65 EUR
PUTPUT763Sound and Efficient Functional Reactive Programming01.01.201531.12.2016Wolfgang JeltschTallinn University of Technology , Institute of Cybernetics at TUT100 560,00 EUR
ETFETF9475Mathematical structures in programming languages01.01.201231.03.2016Tarmo UustaluTallinn University of Technology , Institute of Cybernetics at TUT33 984,00 EUR
SFSF0140007s12Dependable software and human language technologies01.01.201231.12.2014Tarmo UustaluTallinn University of Technology , Institute of Cybernetics at TUT514 620,00 EUR