In a nutshell

Formalize and verify a algorithm using techniques from dependently typed programming.

Background & 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, others qmore expressive and flexible, etc.

It’s clear that 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 is to find a sweet spot of languages that offer strong and static correctness guarantees, while not being too expressive, like requiring full manual verfication, to keep 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, Cayenne, Chameleon, and probably some more.

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.

Requirements

Recommended knowledge includes acquaintance or at least interest with areas like programming language semantics, type theory, programming logics.