Hi! I'm Komi Golova (she/her). I work at JetBrains, where I teach university students and do research on Kotlin.

My research is centered around three topics:

• Formal verification of Kotlin using our SnaKt compiler plugin, which translates Kotlin to Viper
• A uniqueness type system for Kotlin that allows imposing constraints on aliasing.
• Formal semantics for Kotlin in Lean.

I am in the process of finishing my PhD at Radboud University Nijmegen under the supervision of Sebastiaan A. Terwijn and Herman Geuvers.

I live in Utrecht, the Netherlands, but am frequently in Bremen, Germany for work.

Note: this site is still very much WIP.