Making Arbitrary Relational Calculus Queries Safe-Range by Martin Raszyk 📧 and Dmitriy Traytel 🌐 Sep 28
Formalization of Timely Dataflow's Progress Tracking Protocol by Matthias Brun, Sára Decova, Andrea Lattuada 🌐 and Dmitriy Traytel 🌐 Apr 13
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
An Abstract Formalization of Gödel's Incompleteness Theorems 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
A Zoo of Probabilistic Systems by Johannes Hölzl 🌐, Andreas Lochbihler 🌐 and Dmitriy Traytel 🌐 May 27
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions by Dmitriy Traytel 🌐 and Tobias Nipkow 🌐 Jun 12
Abstract Completeness by Jasmin Christian Blanchette 🌐, Andrei Popescu 🌐 and Dmitriy Traytel 🌐 Apr 16
Unified Decision Procedures for Regular Expression Equivalence by Tobias Nipkow 🌐 and Dmitriy Traytel 🌐 Jan 30