P. Jansson was the PhD advisor of U. Norell from 2002 to his PhD degree in 2007.
The PhD thesis (Towards a practical programming language based on dependent type theory, Google Scholar) is often used a the standard reference for the programming language and interactive theorem prover Agda.