Dmitriy Traytel
Homepages π
Entries
2025
2024
A Verified Proof Checker for Metric First-Order Temporal Logic
by Andrei Herasimau, Jonathan Julian Huerta y Munive π§, Leonardo Lima, Martin Raszyk π§ and Dmitriy Traytel π
2023
Pushdown Systems
by Anders Schlichtkrull π, Morten Konggaard Schou, JiΕΓ Srba π and Dmitriy Traytel π
Labeled Transition Systems
by Anders Schlichtkrull π, Morten Konggaard Schou, JiΕΓ Srba π and Dmitriy Traytel π
2022
Making Arbitrary Relational Calculus Queries Safe-Range
by Martin Raszyk π§ and Dmitriy Traytel π
2021
Formalization of Timely Dataflow's Progress Tracking Protocol
by Matthias Brun, SΓ‘ra Decova, Andrea Lattuada π and Dmitriy Traytel π
2020
From Abstract to Concrete GΓΆdel's Incompleteness TheoremsβPart II
by Andrei Popescu π and Dmitriy Traytel π
From Abstract to Concrete GΓΆdel's Incompleteness TheoremsβPart I
by Andrei Popescu π and Dmitriy Traytel π
An Abstract Formalization of GΓΆdel's Incompleteness Theorems
by Andrei Popescu π and Dmitriy Traytel π
A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm
by Ben Fiedler π§ and Dmitriy Traytel π
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
by Lukas Heimes, Dmitriy Traytel π and Joshua Schneider
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
by Thibault Dardinier, Lukas Heimes, Martin Raszyk π§, Joshua Schneider π§ and Dmitriy Traytel π
2019
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
by Joshua Schneider π§ and Dmitriy Traytel π
2018
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull π, Jasmin Christian Blanchette π§ and Dmitriy Traytel π
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull π, Jasmin Christian Blanchette π§, Dmitriy Traytel π and Uwe Waldmann π§
2017
Operations on Bounded Natural Functors
by Jasmin Christian Blanchette π§, Andrei Popescu π and Dmitriy Traytel π
Abstract Soundness
by Jasmin Christian Blanchette π§, Andrei Popescu π and Dmitriy Traytel π
2016
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette π§, Mathias Fleury π§ and Dmitriy Traytel π
2015
A Zoo of Probabilistic Systems
by Johannes HΓΆlzl π, Andreas Lochbihler π and Dmitriy Traytel π
2014
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
by Dmitriy Traytel π and Tobias Nipkow π
Abstract Completeness
by Jasmin Christian Blanchette π, Andrei Popescu π and Dmitriy Traytel π
Unified Decision Procedures for Regular Expression Equivalence
by Tobias Nipkow π and Dmitriy Traytel π