Publications

• Free Foil: Generating Efficient and Scope-Safe Abstract Syntax ICCQ 2024 — 4th International Conference on Code Quality, Innopolis, Russia April 22, 2024
  Joint work with Renata Shakirova, Egor Shalagin, and Karina Tyulebaeva.
• Formalizing the ∞-Categorical Yoneda Lemma CPP 2024 — 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, London, UK January 15, 2024
  Joint work with Emily Riehl and Jonathan Weinberger.
• Free Monads, Intrinsic Scoping, and Higher-Order Preunification TFP 2024 — Trends in Functional Programming, South Orange, NJ, USA January 10, 2024
  2024 John McCarthy Best Paper Award (TFP)
• Teaching Type Systems Implementation with Stella, an Extensible Statically Typed Programming Language TFPiE 2024 — 13th Workshop on Trends in Functional Programming in Education, South Orange, NJ, USA January 9, 2024
  Joint work with Abdelrahman Abounegm and Alexey Stepanov.
• E-Unification for Second-Order Abstract Syntax FSCD 2023 — 8th International Conference on Formal Structures for Computation and Deduction, Rome, Italy July 3, 2023
• Running Regular Research Seminar Online AMSTA 2023 — Agents and Multi-agent Systems: Technologies and Applications, Singapore June 14, 2023
  Joint work with N. V. Shilov, D. A. Kondratyev, and I. S. Anureev.
• Formalizing φ-Calculus: A Purely Object-Oriented Calculus of Decorated Objects FTfJP 2022 — 24th ACM International Workshop on Formal Techniques for Java-like Programs, Berlin, Germany June 7, 2022
  Joint work with Violetta Sim.
• Teaching Logic, from a Conceptual Viewpoint Frontiers in Software Engineering Education 2020 November 1, 2020
  Joint work with Daniel de Carvalho.

Preprints & Workshop Abstracts

• Generic Second-Order Matching, Higher-Order Preunification and Pattern Unification — Implementations in Haskell UNIF 2025 — 39th International Workshop on Unification, Birmingham, UK July 15, 2025
  Joint work with Artem Starikov, Fedor Ivanov, and Damir Afliatonov.
• Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax WITS 2025 — Workshop on Implementation Techniques for Semantics, co-located with POPL 2025, Denver, CO, USA January 25, 2025
  Joint work with Anastasia Smirnova, Vladislav Deryabkin, Diana Tomilovskaia, and Ekaterina Maksimova.
• Towards Generic Higher-Order Unification Implementations in Haskell WITS 2025 — Workshop on Implementation Techniques for Semantics, co-located with POPL 2025, Denver, CO, USA January 25, 2025
  Joint work with Artem Starikov, Fedor Ivanov, and Damir Afliatonov.
• typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell miniKanren '24 — 2024 miniKanren and Relational Programming Workshop, co-located with ICFP 2024, Milan, Italy September 6, 2024
  Joint work with Artem Starikov.
• Deriving Higher-Order Unification in Haskell WITS 2023 — Workshop on Implementation Techniques for Semantics, co-located with IFL 2023, Braga, Portugal August 28, 2023
• Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax UNIF 2023 — 37th International Workshop on Unification, Rome, Italy July 4, 2023
• Experimental Prover for Tope Logic SCAN 2023 — Workshop on Semantical and Computational Aspects of Non-Classical Logics, Moscow, Russia June 16, 2023
• Higher-Order Unification from E-Unification with Second-Order Equations and Parametrised Metavariables UNIF 2022 — 36th International Workshop on Unification, Haifa, Israel August 5, 2022