Proving the Equivalence of Higher-Order Terms by Means of Supercompilation. - Ilya G. Klyuchnikov; Sergei A. Romanenko (Ershov Memorial Conference, 2009)

Multi-result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. - Ilya G. Klyuchnikov; Sergei A. Romanenko (Ershov Memorial Conference, 2011)

Higher-level supercompilation as a metasystem transition. - Ilya G. Klyuchnikov; Sergei A. Romanenko (Program. Comput. Softw., 2012)

Certifying Supercompilation for Martin-Löf's Type Theory. - Ilya G. Klyuchnikov; Sergei A. Romanenko (Ershov Memorial Conference, 2014)

Supercompilation for Martin-Lof's type theory. - Ilya G. Klyuchnikov; Sergei A. Romanenko (Program. Comput. Softw., 2015)

eqWAlizer: scaling Erlang development at WhatsApp with static typing (keynote). - Ilya G. Klyuchnikov (Erlang Workshop, 2022)