I’m a postdoc at the University of Cambridge, in Jon Sterling’s research group. Previously I was a postdoc at the Logic and Types unit in the University of Gothenburg. I did my PhD studies at the Eötvös Loránd University of Budapest, supervised by Ambrus Kaposi.
My research topics are generally related to type theory, ranging from “applied” type theory (compilation, elaboration, performance, metaprogramming) to more “pure” type theory (metatheory of inductive types, universes).
Updates & stuff
- 01/09/26: started a postdoc at the University of Cambridge in Jon Sterling’s research group.
- 13/02/26: slides from my talk at TFP 2026. It’s about two-level TT, with a practical focus, also touching on region allocation.
- 21/01/26: WITS 2026 slides and abstract about using observational equality for postponed unification problems in elaboration.
- 02/12/25: paper about canonicity for indexed inductive-recursive types, to appear at POPL 2026.
- 20/04/25: EuroProofNet working group 6 meeting slides about a generalized logical framework.
- 26/01/25: WITS 2025 slides and abstract about eta conversion for the unit type.
- 21/11/24: a demo project about combining dependent types and runtime code generation.
- 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: WITS 2024 slides and abstract about definition unfolding in elaboration.
- 2/11/23: (belated) slides of WITS 2023 workshop talk about generalizing Miller pattern unification, with an algorithm called “nested pattern unification”. 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.