Hello there!

Glad to see you here, I hope you are doing great!

I am an Assistant Professor at Innopolis University in Russia, where I teach «Programming in Haskell», «Programming Paradigms», «Data Structures and Algorithms», and «Advanced Compilers Construction and Program Analysis».

My research is on type theory and functional programming, mostly:

• Synthetic ∞-category theory — I develop rzk, an experimental proof assistant for the simplicial extension of homotopy type theory, and contribute to sHoTT, an open-source library of formalizations in rzk (including the ∞-categorical Yoneda lemma, joint work with Emily Riehl and Jonathan Weinberger, CPP 2024).
• Higher-order unification and second-order abstract syntax — including E-unification for SOAS (FSCD 2023) and the free-foil library, which generates efficient, scope-safe abstract syntax (ICCQ 2024, TFP 2024).
• Type-system implementation and teaching — including Stella, an extensible statically typed language used as a teaching vehicle for type-system implementation (TFPiE 2024).

On the industry side, I am the CTO and co-founder of getads (formerly GetShop.TV), an interactive-television advertising platform whose backend is powered by Haskell.

If you want the formal version, see my publications and talks.