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 Apr 16
Pushdown Systems by Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel Oct 31
Labeled Transition Systems by Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel Oct 31
Formalization of Timely Dataflow's Progress Tracking Protocol by Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel Apr 13
An Abstract Formalization of Gödel's Incompleteness Theorems by Andrei Popescu and Dmitriy Traytel Sep 16
From Abstract to Concrete Gödel's Incompleteness Theorems—Part II by Andrei Popescu and Dmitriy Traytel Sep 16
From Abstract to Concrete Gödel's Incompleteness Theorems—Part I by Andrei Popescu and Dmitriy Traytel Sep 16
A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm by Ben Fiedler and Dmitriy Traytel Jul 21
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows by Lukas Heimes, Dmitriy Traytel and Joshua Schneider Apr 10
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 Apr 09
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic by Joshua Schneider and Dmitriy Traytel Jul 04
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel Nov 23
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann Jan 18
Operations on Bounded Natural Functors by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel Dec 19
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel Nov 12
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions by Dmitriy Traytel and Tobias Nipkow Jun 12
Unified Decision Procedures for Regular Expression Equivalence by Tobias Nipkow and Dmitriy Traytel Jan 30