Address
Dmitriy Traytel
Institute of Information Security
Department of Computer Science
ETH Zürich
Universitätstrasse 6
8092 Zürich, Switzerland
Office: CAB F 57.2
Phone: +41 44 632 30 23
Email: traytel inf.ethz.ch
Dmitriy Traytel
Starting from August 2015, I am a postdoc 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, decision procedures,
(co)inductive datatypes, and interactive theorem proving. You may want to take a
look at my
(draft) publications,
students I have (co)supervised / am (co)supervising, and
some projects I was/am involved in.
Drafts
Publications
Journal Articles
Conference Papers

Formal Languages, Formally and Coinductively
DT.
In Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), 2016, to appear.

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, Springer, 2015, 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
[slides, official copy]
 M.Sc.

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

Extension of a Type Inference Algorithm with
Coercive Subtyping
[slides]
Student (Co)supervision
Current
 Fabian Meier (M.Sc.)
Nonuniform Datatypes in Isabelle/HOL.
Past
 Julian Biendarra (B.Sc., cosupervisor: Lars Hupel)
FunctorPreserving Type Definitions.
 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.
Projects

Isabelle—a generic proof
assistant

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
(Co)organized Events
© 2011–2015 by Dmitriy Traytel