Dima Szamozvancev

I am a postdoctoral researcher with Dr Jeremy Yallop on the Modular Macros project, investigating the extension of OCaml with macros and metaprogramming features.

I'm also finishing a PhD in the Programming, Logic and Semantics group of the Department of Computer Science and Technology, supervised by Prof. Marcelo Fiore and Dr Neel Krishnaswami. My research focuses on the mathematical theory and computer formalisation of second-order abstract syntax.

In addition, I am a College Associate Professor and Fellow in Computer Science at Downing College, as well as a Director of Studies for IB students. I did my undergraduate (2014–2017) and Master's (2017–2018) studies there as well.

Research

Publications

• Marcelo Fiore, Dmitrij Szamozvancev (2021).
  Formal Metatheory of Second-Order Abstract Syntax
  In: Proceedings of the ACM on Programming Languages 6.POPL (2022): 1-29. Distinguished Paper at POPL 2022. (doi, pdf)
• Christial Uldal Graulund, Dmitrij Szamozvancev, and Neel Krishnaswami (2021).
  Adjoint Reactive GUI Programming.
  In: Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science, vol 12650. Springer, Cham. (doi, arXiv)
• Dmitrij Szamozvancev and Michael B. Gale (2017).
  Well-typed music does not sound wrong (experience report).
  In: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell. ACM, pp. 99–104. (doi, pdf)

Talks

• Functorial models of scope-safe syntax.
  Invited talk at the EuroProofNet WG6 meeting in KU Leuven, April 2024. (pdf)
• Formal Metatheory of Second-Order Abstract Syntax.
  Talk accompanying the paper presented at POPL 2022, held in Philadelphia, January 2022. (pdf)
• Embedded Domain-Specific Languages.
  Guest lecture for the CS141 – Functional Programming course at the University of Warwick, March 2019. (pdf)
• Semantics of temporal type systems.
  Master's research project presentation at the University of Cambridge, June 2018. (pdf)
• Well-typed music does not sound wrong.
  Talk accompanying the paper presented at the Haskell Symposium 2017, held at the University of Oxford, September 2017. (pdf)

Reports and dissertations

• Semantics of temporal type systems.
  Master's dissertation supervised by Dr Neel Krishnaswami. University of Cambridge, 2018. (pdf)
• Well-typed music does not sound wrong.
  Undergraduate dissertation supervised by Michael B. Gale. University of Cambridge, 2017. (pdf)

Academic activities

• FARM 2019 program committee member

Teaching

Supervisions

This year (2024–2025) I am supervising the following courses:

• Foundations of Computer Science
• Discrete Mathematics
• Semantics of Programming Languages
• Logic and Proof
• Computation Theory
• Concepts in Programming Languages
• Types
• Denotational Semantics

Part II project students

• LT Stockmann (2024-2025)
  Formalising an extension of the OCaml module system with macros in Agda
• Anant Gupta (2024-2025)
  Formalisation of the Functional Machine Calculus in Agda
• Peter Wild (2023-2024)
  An Imperative Language for Metaprogramming
• Rokas Urbonas (2023-2024)
  Implementing a higher-order choreographic language
• Patrick Nickols (2022-2023)
  Formalising PCF and its Denotational Semantics in Agda
• Ted While (2020-2021)
  Formalisation of the Dual Calculus in Agda
• James Rhodes (2019-2020)
  Metaprogramming for Automated Frontend Generation

Part III project students

• Gregor Feierabend (2023-2024), co-supervised with Marcelo Fiore
  Second-Order Rewriting: Theory and Mechanisation
• Nissim Chekroun (2021-2022), co-supervised with Marcelo Fiore
  Formalising Contextual Modal Typed Calculi

Contact

• Email: ds709cst.cam.ac.uk
• Department Office: FS13
• College Office: T2