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 have three papers with them:

• Herman Geuvers and Komi Golova. Positive Hennessy-Milner Logic for Branching Bisimulation. Logical Methods in Computer Science, 21(4), paper 14, 2025. arXiv:2210.07380.
• Komi Golova and Sebastiaan A. Terwijn. Embeddings between Partial Combinatory Algebras. Notre Dame Journal of Formal Logic, 64(1):129–158, 2023. arXiv:2204.03553.
• Komi Golova and Sebastiaan A. Terwijn. Fixpoints and relative precompleteness. Computability, 11(2):135–146, 2022. arXiv:2101.12271.