Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus. - Vladimir Komendantsky (MFCSIT, 2006)

Fixed point semantics and partial recursion in Coq. - Yves Bertot; Vladimir Komendantsky (PPDP, 2008)

Interfacing Coq + SSReflect with GAP. - Vladimir Komendantsky; Alexander Konovalov 001; Steve Linton (UITP, 2010)

View of Computer Algebra Data from Coq. - Vladimir Komendantsky; Alexander Konovalov 001; Steve Linton (Calculemus/MKM, 2011)

Subtyping by Folding an Inductive Relation into a Coinductive One. - Vladimir Komendantsky (Trends in Functional Programming, 2011)

Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect. - Vladimir Komendantsky (PLPV, 2012)

Matching Problem for Regular Expressions with Variables. - Vladimir Komendantsky (Trends in Functional Programming, 2012)