See veebileht kasutab küpsiseid kasutaja sessiooni andmete hoidmiseks. Veebilehe kasutamisega nõustute ETISe kasutustingimustega. Loe rohkem
Olen nõus

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, doktorikraad, 2016, (juh) Tarmo Uustalu, Certification of context-free grammar algorithms (Kontekstivabade grammatikate algoritmide sertifitseerimine), Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
Denis Firsov, magistrikraad, 2012, (juh) Tarmo Uustalu, Certified parsing of regular languages (Regulaarsete keelte sertifitseeritud parsimine), Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
 
 
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

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

Otsi projekti

  • {{item.Name}}
Asutus on projekti finantseerija   Asutus on projekti teostaja  
  • {{searchListItem.Name}}
Kõik   Tavaprojektid   Ülemprojektid   Alamprojektid  
Uus Frascati (2015)
Uus ja vana Frascati (otsing uue järgi väljastab ka seotud vanad)
Kõik
Käimasolevad
Lõppenud
Algus
Hajus
Täpne
Lihtotsing Tühjenda
  • Leitud 7 kirjet
ProgrammLiikNumberNimiProjekti algusProjekti lõppVastutav täitjaAsutusFinantseerijapoolne rahastamine
TKEXCSArvutiteaduse tippkeskus - EXCS07.07.200831.08.2015Tarmo UustaluTallinna Tehnikaülikool; Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut4 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 UustaluTallinna Tehnikaülikool, TTÜ Küberneetika Instituut526 194,00 EUR
1.1.3.EITSA18017IT Akadeemia programmi IKT teaduse toetusmeede perioodiks 2018-2022: Tarkvara usaldusväärsus01.01.201831.12.2022Paweł Maria SobocińskiTallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut1 864 416,00 EUR
TKAlamprojektTAR16013 (EXCITE) (TK148)IT Tippkeskus EXCITE01.09.201601.03.2023Maarja KruusmaaTallinna Tehnikaülikool, Infotehnoloogia teaduskond, Biorobootika keskus; Cybernetica AS2 121 014,65 EUR
PUTPUT763Korrektne ja efektiivne funktsionaalne reaktiivne programmeerimine01.01.201531.12.2016Wolfgang JeltschTallinna Tehnikaülikool, TTÜ Küberneetika Instituut100 560,00 EUR
ETFETF9475Matemaatilised struktuurid programmeerimiskeeltes01.01.201231.03.2016Tarmo UustaluTallinna Tehnikaülikool, TTÜ Küberneetika Instituut33 984,00 EUR
SFSF0140007s12Usaldusväärsed tarkvara- ja inimkeeletehnoloogiad01.01.201231.12.2014Tarmo UustaluTallinna Tehnikaülikool, TTÜ Küberneetika Instituut514 620,00 EUR