Joshua’s CISC 499 projects

1. Type checker implementation

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.

2. Nested incremental programming

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.