BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Croatia
1 × Germany
1 × USA
1 × United Kingdom
Collaborated with:
J.C.Blanchette A.Popescu A.P.0001 T.Nipkow ∅ A.Schlichtkrull U.Waldmann Lorenzo Gheri A.Bouzy A.Lochbihler L.Hupel L.Noschinski
Talks about:
foundat (3) procedur (2) corecurs (2) theorem (2) datatyp (2) verifi (2) formal (2) assist (2) proof (2) order (2)

Person: Dmitriy Traytel

DBLP DBLP: Traytel:Dmitriy

Contributed to:

CSL 20152015
ESOP 20152015
ICFP 20152015
IJCAR 20142014
ICFP 20132013
LICS 20122012
ESOP 20172017
IJCAR 20182018
CADE 20192019
Haskell 20142014
POPL 20192019

Wrote 11 papers:

CSL-2015-Traytel #algebra
A Coalgebraic Decision Procedure for WS1S (DT), pp. 487–503.
ESOP-2015-Blanchette0T #data type
Witnessing (Co)datatypes (JCB, AP, DT), pp. 359–382.
ICFP-2015-Blanchette0T #perspective #proving #recursion
Foundational extensible corecursion: a proof assistant perspective (JCB, AP, DT), pp. 192–204.
IJCAR-2014-Blanchette0T #induction #logic
Unified Classical Logic Completeness — A Coinductive Pearl (JCB, AP, DT), pp. 46–60.
ICFP-2013-TraytelN #regular expression #word
Verified decision procedures for MSO on words based on derivatives of regular expressions (DT, TN), pp. 3–12.
LICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #proving #theorem proving
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
ESOP-2017-BlanchetteBL0T #implementation #proving #recursion
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants (JCB, AB, AL, AP0, DT), pp. 111–140.
IJCAR-2018-SchlichtkrullBT #formal method #order #proving
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (AS, JCB, DT, UW), pp. 89–107.
CADE-2019-0001T #theorem
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems (AP0, DT), pp. 442–461.
Haskell-2014-BlanchetteHNNT #case study #experience #haskell
Experience report: the next 1100 Haskell programmers (JCB, LH, TN, LN, DT), pp. 25–30.
POPL-2019-BlanchetteGPT #bound
Bindings as bounded natural functors (JCB, LG, AP0, DT), p. 34.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.