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
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
Formalization of Generic Authenticated Data Structures by Matthias Brun and Dmitriy Traytel π May 14
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
Abstract Soundness by Jasmin Christian Blanchette π§, Andrei Popescu π and Dmitriy Traytel π Feb 10
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