Address
Dmitriy Traytel
Institute of Information Security
Department of Computer Science
ETH Zürich
Universitätstrasse 6
8092 Zürich, Switzerland
Office: CNB F 107.2
Phone: +41 44 632 30 23
Email: traytel inf.ethz.ch
Dmitriy Traytel
Starting from August 2015, I am a postdoctoral researcher in
the Information Security Group led
by David Basin at the ETH
Zürich. Before that I was a PhD student at the TU München, at
the Chair for Logic and Verification headed
by
Tobias Nipkow. There, I participated in
the graduate school PUMA.
My research interests include logic, automata, runtime verification and monitoring,
decision procedures, (co)inductive datatypes, and interactive theorem proving.
Take a look at my
(draft) publications,
students I have (co)supervised / am (co)supervising,
some tools I have (co)developed / am (co)developing, and scientific events I was involved in.
News
Drafts
Publications
Journal Articles

Soundness and Completeness Proofs by Coinductive Methods
Extended version of the IJCAR 2014 paper
Jasmin Christian Blanchette, Andrei Popescu, DT.
In Journal of Automated Reasoning, 58(1), pp. 149–179, 2017 (published online: Oct. 2016), doi.

Verified Decision Procedures for MSO on Words
Based on Derivatives of Regular Expressions
Extended version of the ICFP 2013 paper
DT, Tobias Nipkow
In Journal of Functional Programming, 25, 2015, doi.
Conference Papers

Foundational Nonuniform (Co)datatypes in HigherOrder Logic
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, DT
In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 2017, to appear.

Almost EventRate Independent Monitoring of Metric Temporal Logic
David Basin, Bhargav Bhatt, DT
In Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Springer, 2017, LNCS 10206, pp. 94–112, doi..

Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, DT
In Yang, H. (ed.) 26th European Symposium on Programming (ESOP 2017), Springer, 2017, LNCS 10201, pp. 111–140, doi.

Formal Languages, Formally and Coinductively
Best Student Paper Award
DT.
In Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), LIPIcs 52, pp. 31:1–31:17, Schloss Dagstuhl–LeibnizZentrum fuer Informatik, 2016, doi.

A Coalgebraic Decision Procedure for WS1S
DT.
In Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), LIPIcs 41, pp. 487–503, Schloss Dagstuhl–LeibnizZentrum fuer Informatik, 2015, doi.

A Formalized Hierarchy of Probabilistic System Types (Proof Pearl)
Johannes Hölzl, Andreas Lochbihler, DT
In Zhang, X., Urban, C. (eds.) 6th Conference on Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 203–220, Springer, 2015, doi.

Foundational Extensible Corecursion
A Proof Assistant Perspective
Jasmin Christian Blanchette, Andrei Popescu, DT
In Reppy, J. (ed.) 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 192–204, ACM, 2015, doi.

Witnessing (Co)datatypes
Jasmin Christian Blanchette, Andrei Popescu, DT
In Vitek, J. (ed.) 24th European Symposium on Programming (ESOP 2015), Springer, 2015, LNCS 9032, pp. 359–382, doi.

Experience Report: The Next 1100 Haskell Programmers
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, DT
In Swierstra, W. (ed.) 2014 ACM SIGPLAN Symposium on Haskell (Haskell 2014), ACM, 2014, doi.

Cardinals in Isabelle/HOL
Jasmin Christian Blanchette, Andrei Popescu, DT
In Klein, G., Gamboa, R. (eds.) 5th Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 111–127, Springer, 2014, doi.

Truly Modular (Co)datatypes for Isabelle/HOL
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny,
Andrei Popescu, DT
In Klein, G., Gamboa, R. (eds.) 5th Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 93–110, Springer, 2014, doi.

Unified Classical Logic Completeness: A Coinductive Pearl
Jasmin Christian Blanchette, Andrei Popescu, DT
In Demri, S., Kapur, D., Weidenbach, C. (eds) 7th International Joint Conference on Automated Reasoning (IJCAR 2014), LNCS 8562, pp. 46–60, Springer, 2014, doi.

Unified Decision Procedures for Regular Expression Equivalence
Tobias Nipkow, DT
In Klein, G., Gamboa, R. (eds.) 5th Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 450–466, Springer, 2014, doi.

Verified Decision Procedures for MSO on
Words Based on Derivatives of Regular Expressions
Functional Pearl
DT, Tobias Nipkow
In Morrisett, G., Uustalu, T. (eds.) 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), pp. 3–12, ACM, 2013, doi.

Foundational, Compositional (Co)datatypes for HigherOrder Logic
DT, Andrei Popescu, Jasmin Christian Blanchette
In 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 596–605, IEEE, 2012, doi.

Extending HindleyMilner Type
Inference with Coercive Structural Subtyping
DT, Stefan Berghofer, Tobias Nipkow
In Yang, H. (ed.) 9th Asian Symposium on Program Languages and Systems (APLAS 2011), LNCS 7078, pp. 89–104, Springer, 2011, doi.
Workshop Papers
Theses
 Ph.D.

Formalizing Symbolic Decision Procedures for Regular Languages
[official copy]
 M.Sc.

A Category Theory Based (Co)datatype Package for Isabelle/HOL
 B.Sc.

Extension of a Type Inference Algorithm with
Coercive Subtyping
Student (Co)supervision
Current
 Tom Sydney Kerckhove (M.Sc.)
Signature Inference for QuickSpec.
 Jan Gilcher (B.Sc., cosupervisor: Andreas Lochbihler)
Conditional Parametricity in Isabelle/HOL.
 Bhargav Bhatt (Ph.D., cosupervisor: David Basin)
EventRate Indepedent Monitoring of Metric Temporal Logic.
Past
 Fabian Meier (M.Sc.)
Nonuniform Datatypes in Isabelle/HOL.
 Julian Biendarra (B.Sc., cosupervisor: Lars Hupel)
FunctorPreserving Type Definitions.
 Anders Schlichtkrull (M.Sc., main supervisors: Jørgen Villadsen, Jasmin Blanchette)
Formalization of Resolution Calculus in Isabelle.
 Aymeric Bouzy (M.Sc. intern, cosupervisor: Jasmin Blanchette)
Nonprimitive Corecursion Support in Isabelle/HOL.
 Mathias Fleury (M.Sc. intern, main supervisor: Jasmin Blanchette)
Formalization of Ground Inference Systems.
 Matthias Franze (B.Sc.)
A PurelyFunctional, ProofProducing, Incremental Algorithm for the Congruence Closure.
 Martin Desharnais (B.Eng., cosupervisor: Jasmin Blanchette)
Formalizing Types and Programming Languages.
 Lorenz Panny (B.Sc., cosupervisor: Jasmin Blanchette)
Primitively (Co)recursive Function Definitions.
Tools
Current

Aerial—an almost eventrate independent monitor for metric temporal logic

Isabelle—a generic proof
assistant

MonaCo—a symbolic coalgebraic decision procedure for
weak monadic secondorder logic of one successor (WS1S)
Past

Hecke—a GAP 4 package for calculating
decomposition matrices of Hecke algebras of the symmetric groups and qSchur
algebras

POTATOES—a small
operating system for x86 platforms
Events
Forthcoming
Past
© 2011–2017 by Dmitriy Traytel