Recursive monadic bindings. - Levent Erkök; John Launchbury (ICFP, 2000)

A recursive do for Haskell. - Levent Erkök; John Launchbury (Haskell, 2002)

Semantics of value recursion for Monadic Input/Output. - Levent Erkök; John Launchbury; Andrew Moran (RAIRO Theor. Informatics Appl., 2002)

Imperative Functional Programming with Isabelle/HOL. - Lukas Bulwahn; Alexander Krauss 001; Florian Haftmann; Levent Erkök; John Matthews (TPHOLs, 2008)

High assurance programming in Cryptol. - Levent Erkök; John Matthews (CSIIRW, 2009)

Hardware/software co-verification of cryptographic algorithms using Cryptol. - Levent Erkök; Magnus Carlsson; Adam Wick (FMCAD, 2009)

Pragmatic equivalence and safety checking in Cryptol. - Levent Erkök; John Matthews (PLPV, 2009)

Practical Considerations in Control-Flow Integrity Monitoring. - Iavor S. Diatchki; Lee Pike; Levent Erkök (ICST Workshops, 2011)

Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs). - Warren E. Ferguson; Jesse Bingham; Levent Erkök; John R. Harrison; Joe Leslie-Hurd (CoRR, 2017)

Digit Serial Methods with Applications to Division and Square Root. - Warren E. Ferguson; Jesse Bingham; Levent Erkök; John R. Harrison; Joe Leslie-Hurd (IEEE Trans. Computers, 2018)