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
- 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.