Static type checking is a lightweight formal method: in safe languages like Haskell, OCaml and Java, passing the type checker guarantees that certain errors cannot occur. More expressive type systems allow more precise properties to be checked, ruling out a larger class of errors.
Designing and implementing more expressive type systems is a major research challenge. However, type inference—which relieves the user of writing type declarations—is impossible (undecidable) for most such systems. Bidirectional type systems overcome the decidability barrier: they combine type inference with type checking, yielding much of the convenience of type inference along with greater expressiveness.
Previously, I developed a bidirectional typing algorithm (Dunfield and Krishnaswami, ICFP 2013) that supports a particular kind of generic programming—higher-rank polymorphism. Several third parties have implemented versions of this algorithm, but we don't have an implementation of our own to try out and build on. For this project, you would implement that algorithm and, probably, some extensions to it (to be determined).
Functional programming languages are well-suited to this project, so experience with Haskell, OCaml, or another functional programming language would be helpful. I will work with you to give the background needed to read the paper and understand the algorithm. If you enjoyed CISC 260, you should consider this project.
A more ambitious variant of project 1 would involve a type system currently being designed by me and Neel Krishnaswami (University of Cambridge). This system reformulates liquid types, attempting to better understand their theoretical foundations and how those foundations result in decidable and practical type-checking. This project may also include opportunities for more theoretical work.
Gradual typing allows programmers to combine different "levels" of typing in one program, module, or even within a single function—combining dynamic typing and static typing, or static typing and refinement typing.
Pursuing a unified type mechanism for gradual typing has led to a new type system and an unusual operational semantics, so implementing both a type checker (for the type system) and an interpreter (for the operational semantics) could answer two questions: (1) whether type checking in this system is practical, and (2) whether the operational semantics is realistic, or can be made realistic.
In terms of "ambition level", this project probably falls between 1 and 2 above.
An incremental program remembers intermediate results, reusing them when possible. When the input to the program changes slightly, most of the work is reused, resulting in often-impressive speedups over running the program "from scratch". For example, if you have already sorted a list of n records in O(n log n), you can add a new record in O(n) time: walk through the sorted list and insert the new record in the correct place.
This incremental program required some insight into the problem domain. For larger programs, figuring out new incremental algorithms can be very hard; people sometimes receive PhDs for designing a single new incremental algorithm!
Programming languages research offers an easier path: we have built compilers that automatically incrementalize many programs. However, our existing approaches do not scale to large programs. We don't know how to account for incremental programs that are nested: run inside other incremental programs.
In this project, you would find examples of nested incremental programs, implement one or more, and evaluate their performance (e.g. measuring speedups). Experience with a functional programming language, e.g. Haskell or OCaml, or with Rust, would be helpful. An interest in programming languages and/or algorithms is desirable.