We are advertising several PhD positions at Nottingham which includes the Functional Programming Laboratory.
The group which includes Nicolai Kraus and Ulrik Buchholtz has got a strong interest in Type Theory in particular Homotopy Type Theory and its semantic foundations using (higher) category theory. We mainly use the agda system for formal developments.
If you are interested, please contact me before applying.
Cheers,
Thorsten