Dmitriy Traytel
According to our database^{1},
Dmitriy Traytel
authored at least 44 papers
between 2011 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at orcid.org
On csauthors.net:
Bibliography
2019
Bindings as bounded natural functors.
PACMPL, 2019
Formalization of a Monitoring Algorithm for Metric FirstOrder Temporal Logic.
Archive of Formal Proofs, 2019
Formalization of Generic Authenticated Data Structures.
Archive of Formal Proofs, 2019
Generic Authenticated Data Structures, Formally.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019
From Nondeterministic to MultiHead Deterministic FiniteState Transducers.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019
A verified prover based on ordered resolution.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.
Proceedings of the Automated Deduction  CADE 27, 2019
2018
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover.
Archive of Formal Proofs, 2018
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover.
Archive of Formal Proofs, 2018
Scalable Online FirstOrder Monitoring.
Proceedings of the Runtime Verification  18th International Conference, 2018
A Taxonomy for Classifying Runtime Verification Tools.
Proceedings of the Runtime Verification  18th International Conference, 2018
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.
Proceedings of the Automated Reasoning  9th International Joint Conference, 2018
Optimal Proofs for Linear Temporal Logic on Lasso Words.
Proceedings of the Automated Technology for Verification and Analysis, 2018
2017
Soundness and Completeness Proofs by Coinductive Methods.
J. Autom. Reasoning, 2017
Operations on Bounded Natural Functors.
Archive of Formal Proofs, 2017
Abstract Soundness.
Archive of Formal Proofs, 2017
Almost EventRate Independent Monitoring of Metric Temporal Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017
AERIAL: Almost EventRate Independent Algorithms for Monitoring Metric Regular Properties.
Proceedings of the RVCuBES 2017. An International Workshop on Competitions, 2017
Almost EventRate Independent Monitoring of Metric Dynamic Logic.
Proceedings of the Runtime Verification  17th International Conference, 2017
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017
Foundational nonuniform (Co)datatypes for higherorder logic.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017
Foundational (Co)datatypes and (Co)recursion for HigherOrder Logic.
Proceedings of the Frontiers of Combining Systems  11th International Symposium, 2017
Friends with Benefits  Implementing Corecursion in Foundational Proof Assistants.
Proceedings of the Programming Languages and Systems, 2017
A Report of ARCADE 2017.
Proceedings of the ARCADE 2017, 2017
2016
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals.
Archive of Formal Proofs, 2016
Formal Languages, Formally and Coinductively.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016
2015
Formalizing Symbolic Decision Procedures for Regular Languages.
PhD thesis, 2015
Derivatives of Logical Formulas.
Archive of Formal Proofs, 2015
A Zoo of Probabilistic Systems.
Archive of Formal Proofs, 2015
A Formalized Hierarchy of Probabilistic System Types  Proof Pearl.
Proceedings of the Interactive Theorem Proving  6th International Conference, 2015
Foundational extensible corecursion: a proof assistant perspective.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015
Witnessing (Co)datatypes.
Proceedings of the Programming Languages and Systems, 2015
A Coalgebraic Decision Procedure for WS1S.
Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015
2014
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions.
Archive of Formal Proofs, 2014
Abstract Completeness.
Archive of Formal Proofs, 2014
Unified Decision Procedures for Regular Expression Equivalence.
Proceedings of the Interactive Theorem Proving  5th International Conference, 2014
Truly Modular (Co)datatypes for Isabelle/HOL.
Proceedings of the Interactive Theorem Proving  5th International Conference, 2014
Cardinals in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving  5th International Conference, 2014
Experience report: the next 1100 Haskell programmers.
Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014
Unified Classical Logic Completeness  A Coinductive Pearl.
Proceedings of the Automated Reasoning  7th International Joint Conference, 2014
2013
A Codatatype of Formal Languages.
Archive of Formal Proofs, 2013
Verified decision procedures for MSO on words based on derivatives of regular expressions.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013
2012
Foundational, Compositional (Co)datatypes for HigherOrder Logic: Category Theory Applied to Theorem Proving.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012
2011
Extending HindleyMilner Type Inference with Coercive Structural Subtyping.
Proceedings of the Programming Languages and Systems  9th Asian Symposium, 2011