Background and motivation
Type systems in programming languages have been around, like, forever. Basically every programming language has types and a type system, in one form or another, some more visible to the user, some less, some more rigid, some more expressive and flexible etc.
It's clear that historically the overall trend is towards more expressive type systems (and systems can be /very/ expressive indeed, repesenting full-fleged, higher order logics). The connection between type systems and logics is known since long; it is also exploited in type-based theorem provers, tools offer computer-aided proof assistance. Tools along this direction have reached quite some maturity.
The spectrum ranging from the basic and limited bread-and-butter type systems (``int'' and ``bool'' and ``arrays'') from languages of yore to full-blown, heavy-duty theorem provers.
More recently, there had been a trend toward programming languages or extensions that offer expressiveness well-beyond standard type system but without going all the way toward theorem proving. They ``slogan'' there is *dependently typed programming languages* or *type-level programming*.
The hope there is to find a sweet spot of languages that offer strong and static correctness guarantees, while not being too expressive, like offering fully veryfied verfication, as keeping the spirit of traditional type checking, namely being automatic. There are quite many languages or design proposals out, examples include Liquid Haskell (or ``liquid'' extensions of other languages), dependent Haskell, Epigram, Agda, Idris, ATS, Cayenned, Chameleon, and probably some more.
Problem setting
A thesis in the area is to use one such language and apply it to some interesting algorithm, and use the expressivity to establish relevant properties.
There are different areas, that could be used as source for problems, one could be /security/, for instance, from language-based security.
Also possible could be: take one problem and encode it in different frameworks, and compare their usability, maturity etc.