Dmitriy Traytel

According to our database1, Dmitriy Traytel authored at least 39 papers between 2011 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Bindings as bounded natural functors.
PACMPL, 2019

A verified prover based on ordered resolution.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 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 First-Order 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 Event-Rate Independent Monitoring of Metric Temporal Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Almost Event-Rate 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 higher-order logic.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order 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 Higher-Order Logic: Category Theory Applied to Theorem Proving.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

2011
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011


  Loading...