Edit Profile (opens in new tab) Traytel, Dmitry Compute Distance To: Compute Author ID: traytel.dmitry Published as: Traytel, Dmitriy; Traytel, Dmitry Documents Indexed: 32 Publications since 2012 Co-Authors: 40 Co-Authors with 29 Joint Publications 581 Co-Co-Authors all top 5 Co-Authors 3 single-authored 13 Blanchette, Jasmin Christian 12 Popescu, Andrei 6 Basin, David A. 6 Lochbihler, Andreas 5 Krstić, Srđan 4 Schneider, Joshua P. 3 Hölzl, Johannes 3 Nipkow, Tobias 3 Raszyk, Martin 2 Bhatt, Bhargav Nagaraja 2 Bouzy, Aymeric 2 Fleury, Mathias 2 Fürer, Basil 2 Meier, Fabian 2 Panny, Lorenz 2 Schlichtkrull, Anders 2 Waldmann, Uwe 1 Ahrendt, Wolfgang 1 Bartocci, Ezio 1 Bianculli, Domenico 1 Biendarra, Julian 1 Brix, Frederik 1 Brun, Matthias 1 Colombo, Christian 1 Dardinier, Thibault 1 Desharnais, Martin 1 Falcone, Yliès 1 Francalanza, Adrian 1 Heimes, Lukas 1 Kunčar, Ondřej 1 Lourenço, João M. 1 Nickovic, Dejan 1 Pace, Gordon J. 1 Rufino, José 1 Sánchez, César 1 Schneider, Gerardo 1 Signoles, Julien 1 Sternagel, Christian 1 Thiemann, René 1 Weiss, Alexander Serials 3 Journal of Automated Reasoning 2 Formal Methods in System Design 2 Logical Methods in Computer Science 1 Journal of Functional Programming Fields 31 Computer science (68-XX) 15 Mathematical logic and foundations (03-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 23 Publications have been cited 150 times in 81 Documents Cited by ▼ Year ▼ Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C. 13 2012 Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 11 2015 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe 10 2018 Unified decision procedures for regular expression equivalence. Zbl 1416.68175Nipkow, Tobias; Traytel, Dmitriy 10 2014 Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 10 2014 Soundness and completeness proofs by coinductive methods. Zbl 1409.68251Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 8 2017 A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy 8 2015 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy 6 2017 Cardinals in Isabelle/HOL. Zbl 1416.68152Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 6 2014 A coalgebraic decision procedure for WS1S. Zbl 1373.03015Traytel, Dmitriy 4 2015 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 4 2020 A survey of challenges for runtime verification from advanced application domains (beyond software). Zbl 1425.68268Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander 4 2019 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346Traytel, Dmitriy; Nipkow, Tobias 4 2013 A formally verified abstract account of Gödel’s incompleteness theorems. Zbl 07178991Popescu, Andrei; Traytel, Dmitriy 3 2019 Witnessing (co)datatypes. Zbl 1335.68224Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 3 2015 Almost event-rate independent monitoring. Zbl 1425.68249Basin, David; Bhatt, Bhargav Nagaraja; Krstić, Srđan; Traytel, Dmitriy 3 2019 Formal languages, formally and coinductively. Zbl 1387.68161Traytel, Dmitriy 2 2016 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049Traytel, Dmitriy; Nipkow, Tobias 1 2015 Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy 1 2017 Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy 1 2017 Multi-head monitoring of metric temporal logic. Zbl 1437.68119Raszyk, Martin; Basin, David; Krstić, Srđan; Traytel, Dmitriy 1 2019 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 4 2020 A survey of challenges for runtime verification from advanced application domains (beyond software). Zbl 1425.68268Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander 4 2019 A formally verified abstract account of Gödel’s incompleteness theorems. Zbl 07178991Popescu, Andrei; Traytel, Dmitriy 3 2019 Almost event-rate independent monitoring. Zbl 1425.68249Basin, David; Bhatt, Bhargav Nagaraja; Krstić, Srđan; Traytel, Dmitriy 3 2019 Multi-head monitoring of metric temporal logic. Zbl 1437.68119Raszyk, Martin; Basin, David; Krstić, Srđan; Traytel, Dmitriy 1 2019 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe 10 2018 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 Soundness and completeness proofs by coinductive methods. Zbl 1409.68251Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 8 2017 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy 6 2017 Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy 1 2017 Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy 1 2017 Formal languages, formally and coinductively. Zbl 1387.68161Traytel, Dmitriy 2 2016 Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 11 2015 A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy 8 2015 A coalgebraic decision procedure for WS1S. Zbl 1373.03015Traytel, Dmitriy 4 2015 Witnessing (co)datatypes. Zbl 1335.68224Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 3 2015 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049Traytel, Dmitriy; Nipkow, Tobias 1 2015 Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Unified decision procedures for regular expression equivalence. Zbl 1416.68175Nipkow, Tobias; Traytel, Dmitriy 10 2014 Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 10 2014 Cardinals in Isabelle/HOL. Zbl 1416.68152Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 6 2014 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346Traytel, Dmitriy; Nipkow, Tobias 4 2013 Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C. 13 2012 all cited Publications top 5 cited Publications all top 5 Cited by 127 Authors 11 Blanchette, Jasmin Christian 11 Traytel, Dmitry 9 Popescu, Andrei 8 Lochbihler, Andreas 4 Abel, Andreas M. 4 Fleury, Mathias 4 Holík, Lukáš 4 Kunčar, Ondřej 4 Lengál, Ondřej 4 Schlichtkrull, Anders 4 Vojnar, Tomáš 4 Waldmann, Uwe 3 Basin, David A. 3 From, Asta Halkjær 3 Lammich, Peter 3 Moreira, Nelma 3 Reis, Rogério 3 Schneider, Joshua P. 3 Tourret, Sophie 3 Villadsen, Jørgen 2 Broda, Sabine 2 Brunner, Julian 2 Desharnais, Martin 2 Doczkal, Christian 2 Fiedor, Tomáš 2 Foster, Simon 2 Fürer, Basil 2 Havlena, Vojtěch 2 Krstić, Srđan 2 Momigliano, Alberto 2 Pientka, Brigitte 2 Pous, Damien 2 Raszyk, Martin 2 Reynolds, Andrew 2 Robillard, Simon 2 Smolka, Gert 2 Thiemann, Peter J. 2 Weidenbach, Christoph 1 Adelsberger, Stephan 1 Allais, Guillaume 1 Avigad, Jeremy 1 Basold, Henning 1 Bauereiß, Thomas 1 Bentkamp, Alexander 1 Blackburn, Patrick 1 Bonacina, Maria Paola 1 Bonakdarpour, Borzoo 1 Borgström, Johannes 1 Bouzy, Aymeric 1 Cini, Clare 1 Cockx, Jesper 1 Cohen, Liron 1 Cruanes, Simon 1 Dardinier, Thibault 1 Divasón, Jose 1 Echenim, Mnacho 1 Eriksson, Lars-Henrik 1 Eschen, Agnes Moesgård 1 Forsberg Gutkovas, Ramūnas 1 Francalanza, Adrian 1 Freitas, Leo 1 Futatsugi, Kokichi 1 Gheri, Lorenzo 1 Gidey, Habtom Kashay 1 Guiol, Hervé 1 Gunther, Emmanuel 1 Hameer, Aliya 1 Hanaoka, Goichiro 1 Heimes, Lukas 1 Holzer, Markus 1 Hölzl, Johannes 1 Hudon, Simon 1 Hupel, Lars 1 Jacquemin, Maxime 1 Janků, Petr 1 Jensen, Alexander Birch 1 Johann, Patricia 1 Joosten, Sebastiaan J. C. 1 Junges, Sebastian 1 Kitagawa, Fuyuki 1 Kosmatov, Nikolai 1 Kuncak, Viktor 1 Larsen, John Bruntse 1 Machiavelo, António 1 Maia, Eva 1 Marmsoler, Diego 1 Matichuk, Daniel 1 Matsuda, Takahiro 1 Murray, Toby 1 Nipkow, Tobias 1 Norrish, Michael 1 Pagano, Miguel 1 Parrow, Joachim 1 Peltier, Nicolas 1 Pesenti Gritti, Armando 1 Polonsky, Andrew 1 Raimondi, Franco 1 Sánchez Terraf, Pedro 1 Sánchez, César 1 Sangiorgi, Davide ...and 27 more Authors all top 5 Cited in 12 Serials 23 Journal of Automated Reasoning 4 Journal of Functional Programming 2 Formal Aspects of Computing 2 AI Communications 2 Logical Methods in Computer Science 1 Acta Informatica 1 Journal of Computer and System Sciences 1 Information and Computation 1 Journal of Cryptology 1 MSCS. Mathematical Structures in Computer Science 1 Formal Methods in System Design 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 8 Fields 78 Computer science (68-XX) 27 Mathematical logic and foundations (03-XX) 3 Information and communication theory, circuits (94-XX) 2 Operations research, mathematical programming (90-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Probability theory and stochastic processes (60-XX) Citations by Year