I’m a postdoc at the Logic and Types group at the University of Gothenburg. Previously I was an assistant lecturer at the Faculty of Informatics of Eötvös Loránd University of Budapest, at the department of Programming Languages and Compilers. I did my PhD studies at the same place from 2017 to 2021 under the supervision of Ambrus Kaposi.

My research topics are generally related to type theory, and they range from “applied” type theory (compilation, elaboration, performance, metaprogramming) to more “pure” type theory (metatheory of inductive types, universes).

Updates & stuff

• 26/09/24: A post about lightweight memory regions in two-stage programming.
• 27/08/24: A note on formalizing correctness of elaboration for type theories.
• 26/06/24: I formalized in Agda a nice & simple refutation of function extensionality that’s due to Pierre-Marie Pédrot.
• 18/06/24: new paper about staged compilation, to appear at ICFP 2024. Code supplement.
• 22/01/23: my WITS 2024 slides and abstract.
• 2/11/23: my (belated) slides from my WITS 2023 workshop talk. Abstract as well.
• 25/10/23: a note about eta conversion for the unit type.
• 9/08/23: a post about garbage collection which has zero cost outside of GC.
• 24/05/23: slides for my HoTT 2023 talk about efficient cubical evaluation
• 20/02/23: a Proof Assistants answer about inductive types in Agda.
• 18/12/22: a note about higher induction-induction-recursion.
• 12/09/22: I defended my thesis.
• New WIP project about cubical evaluation.
• New repo for staged fusion in Haskell.