Formalization of Timely Dataflow's Progress Tracking Protocol
by Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel
Dmitriy Traytel
2021
2020
Syntax-Independent Logic Infrastructure
by Andrei Popescu and Dmitriy Traytel
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
Formalization of Generic Authenticated Data Structures
by Matthias Brun 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