I am interested in Martin Löf’s type theory, dependent types, intuitionistic mathematics in general, category theory, and functional programming. I am particularly interested in the semantics of type theory in type theory, and the mathematical structures arising in programming languages and logics.

Current/Recent Events

  1. SPLS 2016 (co-organizer)
  2. TyDe 2016 (co-chair of programme committee)
  3. Agda Intensive Meeting XXII (co-organizer)
  4. TLCA 2015 (member of programme committee)
  5. APLAS 2014 (member of programming committee)
  6. Agda Intensive Meeting XX (co-organizer)