A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. - Heiko Becker; Nikita Zyuzin; Raphaël Monat; Eva Darulova; Magnus O. Myreen; Anthony C. J. Fox (FMCAD, 2018)

Contextual modal types for algebraic effects and handlers. - Nikita Zyuzin; Aleksandar Nanevski (Proc. ACM Program. Lang., 2021)