Dmitriy Traytel

Homepages 🌐

• https://traytel.bitbucket.io/

Entries

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 🌐

Apr 16

2023

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

2022

Making Arbitrary Relational Calculus Queries Safe-Range

by Martin Raszyk 📧 and Dmitriy Traytel 🌐

Sep 28

2021

Formalization of Timely Dataflow's Progress Tracking Protocol

by Matthias Brun, Sára Decova, Andrea Lattuada 🌐 and Dmitriy Traytel 🌐

Apr 13

2020

Syntax-Independent Logic Infrastructure

by Andrei Popescu 🌐 and Dmitriy Traytel 🌐

Sep 16

Robinson Arithmetic

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

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

2019

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

2018

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

2017

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

2016

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

by Jasmin Christian Blanchette 📧, Mathias Fleury 📧 and Dmitriy Traytel 🌐

Nov 12

2015

Derivatives of Logical Formulas

by Dmitriy Traytel 🌐

May 28

A Zoo of Probabilistic Systems

by Johannes Hölzl 🌐, Andreas Lochbihler 🌐 and Dmitriy Traytel 🌐

May 27

2014

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

2013

A Codatatype of Formal Languages

by Dmitriy Traytel 🌐

Nov 15