My name is Moritz Lichter and I was a member of the Programming Systems Lab. I investigated Büchi automata and S1S in constructive type theory (see the project page).