What are other applications of dependent types in programming languages that are similar to sized types?


I’m looking for project ideas for my bachelor thesis that are somehow related to dependent types (the area seems interesting to me and I’d like to get more familiar to type systems in general). Simply implementing a language with such a type system probably isn’t specific enough for this purpose and it may even too broad of a project idea. I’ve been told to look over this paper that talks about using dependent types to check for termination for corecursive functions. So that’s my reference point – what other similarly specific ideas are there out there? I don’t necessarily care as much about practicality as about, well, approachability for someone who has no formal education is language theory but is eager to get into type systems and dependent types.

(Hopefully this post complies with the site’s rules)