Supervision and teaching
Please contact me if you are interested in doing a PhD, master or bachelor thesis with me.
Current PhD supervision
Axel Ljungström - Cubical Methods for Computer Formalization of Mathematics. Started autumn 2020.
Max Zeuner - Cubical type theory and Cubical Agda. Started autumn 2019.
Previous supervision
Master thesis: Axel Ljungström - Computing Cohomology with Cubical Agda. Joint with Guillaume Brunerie at Stockholm University. Awarded Mittag-Leffler prize for excellent master theses at Stockholm University. Defended August 2020.
Master thesis: Elisabeth Bonnevier - Formalizing Cartesian Cubical Sets in UniMath. Awarded Mittag-Leffler prize for excellent master theses at Stockholm University. Defended March 2020.
Master thesis: Zesen Qian - Towards Eilenberg-MacLane Spaces in Cubical Type Theory. Joint with Steve Awodey at Carnegie Mellon University. Defended spring 2019.
Bachelor thesis: Formalization of Algorithms and Mathematical Proofs - Jesper Andersson, Åsa Lideström, Daniel Oom, Anders Sjöberg and Niclas Ståhl implemented and formally verified an implementation of the Took-Cook algorithm for efficient polynomial multiplication using Coq and SSReflect. Chalmers University of Technology. Defended spring 2013.
Teaching at Stockholm University
Upcoming
Programming Paradigms - Spring 2022.
Programming for Mathematicians - Spring 2022.
Current
- Homotopical models of type theories (with Peter LeFanu Lumsdaine) - Autumn 2021.