BSc/MSci projects

Looking for a supervisor for a BSc or MSci project for CS or CS+AI?

My main areas of expertise revolve around the formalization of mathematics or the use of type theory to express ideas from mathematics or programming synthetically (via domain specific languages).

I often use Agda or Lean for formalization, or just work with pen-and-paper.

Here's a list of ideas that we can take as starting points, but please feel free to suggest other topics:

  • Formalize topics from elementary group theory, combinatorics, or geometry in univalent foundations, in the style of the Symmetry book
  • Formalize classical mathematical theorems for Lean's mathlib (preferably something you already understand)
  • Formalize topics from category theory in univalent foundations (maybe for the 1lab)
  • Explore topics within synthetic differential geometry (SDG) in type theory
  • Explore topics within synthetic algebraic geometry in type theory à la Blechschmidt and the Synthetic Geometry project
  • Explore topics within synthetic higher category theory in type theory à la Riehl–Shulman
  • Explore aspects of distributed, probabilistic, or quantum computation by working in an appropriate internal language/type theory
Creative Commons License Work by Ulrik Buchholtz licensed under a Creative Commons Attribution-Noncommercial-Share Alike 4.0 License.