Dmitriy Traytel

 

Website: http://people.inf.ethz.ch/trayteld/

 

Entries

2020

September 16: Syntax-Independent Logic Infrastructure

September 16: Robinson Arithmetic

September 16: From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

September 16: From Abstract to Concrete Gödel's Incompleteness Theorems—Part I

September 16: An Abstract Formalization of Gödel's Incompleteness Theorems

July 21: A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

April 10: Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows

April 9: Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

 

2019

July 4: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

May 14: Formalization of Generic Authenticated Data Structures

 

2018

November 23: A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

January 18: Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

 

2017

December 19: Operations on Bounded Natural Functors

February 10: Abstract Soundness

 

2016

November 12: Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

 

2015

May 28: Derivatives of Logical Formulas

May 27: A Zoo of Probabilistic Systems

 

2014

June 12: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

April 16: Abstract Completeness

January 30: Unified Decision Procedures for Regular Expression Equivalence

 

2013

November 15: A Codatatype of Formal Languages