Lambda Substitution Algebras. - Zinovy Diskin; Ilya Beylin (MFCS, 1993)

Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. - Ilya Beylin; Peter Dybjer (TYPES, 1995)

A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. - Sten Agerholm; Ilya Beylin; Peter Dybjer (TPHOLs, 1996)