Curriculum Vitae

I’m a PhD student at IMDEA Software Institute advised by Niki Vazou and Gilles Barthe.

My research interests are type theory, functional programming, and software verification.

Research

Relational Types for Haskell (PhD thesis)

Designed and implemented an algorithmic relational type system for Haskell as a part of Liquid Haskell project. Currenly, I work on verification of probabilistic Haskell programs using relational typing.

Formal System for LiquidJava (internship with LASIGE)

I’m working on formalizing of a refinement type system for Java with Catarina Gamboa and Alcides Fonseca. The system is based on Featherweight Java and features typestates to control state transitions of objects between method calls.

An Expressive Type System for Stream Processing (undergraduate project)

Designed a type system with row polymorphism for big data processing. Queries such as select *, id from X join Y which contain wildcards and joins particularly benefit from the use of rows.

Translation of Intersection Types to System F (undergraduate project)

Implemented a translation of a typing judgement from a STLC with intersection types to a System F. The translation is sound in the subsystems of rank two. The algorithm is known as antiunification.

Education

2021-2023, Master of Applied Mathematics and Information Sciences at HSE

2018-2021, Bachelor of Applied Mathematics and Information Sciences at HSE

2016-2018, Bachelor of Applied Mathematics and Physics at SPbAU (unfinished, transferred to HSE)

2009-2016, high school graduate from Saint Petersburg Lyceum 30

Training

Jun 2021, Programming Languages Mentoring Workshop @ PLDI

Jun 2021, Oregon Programming Languages Summer School

Jan 2020, VMCAI Winter School on Formal Methods

Oct 2019, Programming Languages Mentoring Workshop @ SPLASH

Jun 2019, Haskell Summer School Monadic Party

Volunteering at Conferences

Jun 2022, PLDI

Feb 2021, Lambda Days

Jan 2021, POPL

Oct 2019, SPLASH

Jul 2019, ECOOP

Industry Internships

2020, Google, Switzerland, created an automatic workflow of requesting computational resources for SaaS clients across Google.

2019, Bloomberg, UK, developed a lock-free debugging utility for caches of a market data distribution network.

2019, Yandex, Russia, improved ranking of user reviews in Yandex search engine. Specifically, supported marketing analytics as an additional source of ranking features.

2018, Google, Poland, implemented user-specific labeling of noteworthy processes in Google’s production monitoring tool.

2017, JetBrains, Russia, developed an auto-smoothing algorithm for low-poly 3D objects in a VR game engine CoSpaces.