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
Labeled Transition Systems
by Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel
2022
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
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
2016
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel
2015
2014
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
by Dmitriy Traytel and Tobias Nipkow