Dmitriy Traytel
Dmitriy Traytel
ETH Zürich
Geverifieerd e-mailadres voor inf.ethz.ch - Homepage
Titel
Geciteerd door
Geciteerd door
Jaar
Truly Modular (Co)datatypes for Isabelle/HOL
JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel
ITP 2014, 93-110, 2014
912014
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
D Traytel, A Popescu, JC Blanchette
LICS 2012, 596-605, 2012
592012
Foundational Extensible Corecursion: A Proof Assistant Perspective
JC Blanchette, A Popescu, D Traytel
ICFP 2015, 192-204, 2015
352015
Almost event-rate independent monitoring of metric dynamic logic
D Basin, S Krstić, D Traytel
International Conference on Runtime Verification, 85-102, 2017
272017
Friends with Benefits: Implementing Foundational Corecursion in Proof Assistants
JC Blanchette, A Bouzy, A Lochbihler, A Popescu, D Traytel
ESOP 2017, 2017
26*2017
Unified Classical Logic Completeness—A Coinductive Pearl
JC Blanchette, A Popescu, D Traytel
IJCAR 2014, 46-60, 2014
26*2014
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
D Basin, BN Bhatt, D Traytel
TACAS 2017, 2017
232017
Witnessing (Co)datatypes
JC Blanchette, A Popescu, D Traytel
ESOP 2015, 359-382, 2015
222015
Unified Decision Procedures for Regular Expression Equivalence
T Nipkow, D Traytel
ITP 2014, 450-466, 2014
192014
Foundational nonuniform (co) datatypes for higher-order logic
JC Blanchette, F Meier, A Popescu, D Traytel
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017
182017
Cardinals in Isabelle/HOL
JC Blanchette, A Popescu, D Traytel
ITP 2014, 111-127, 2014
182014
A taxonomy for classifying runtime verification tools
Y Falcone, S Krstić, G Reger, D Traytel
International Conference on Runtime Verification, 241-262, 2018
172018
Soundness and completeness proofs by coinductive methods
JC Blanchette, A Popescu, D Traytel
Journal of Automated Reasoning 58 (1), 149-179, 2017
172017
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
D Traytel, S Berghofer, T Nipkow
APLAS 2011, 89-104, 2011
172011
Formalizing Bachmair and Ganzinger’s ordered resolution prover
A Schlichtkrull, JC Blanchette, D Traytel, U Waldmann
International Joint Conference on Automated Reasoning, 89-107, 2018
162018
A Formalized Hierarchy of Probabilistic System Types
J Hölzl, A Lochbihler, D Traytel
ITP 2015, 203-220, 2015
152015
Foundational (co) datatypes and (co) recursion for higher-order logic
J Biendarra, JC Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, ...
International Symposium on Frontiers of Combining Systems, 3-21, 2017
142017
A verified prover based on ordered resolution
A Schlichtkrull, JC Blanchette, D Traytel
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
132019
AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.
DA Basin, S Krstic, D Traytel
RV-CuBES, 29-36, 2017
112017
Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
D Traytel, T Nipkow
ICFP 2013, 3-12, 2013
92013
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20