profile pic


PhD Doctor of Philosophy candidate

Proof Assistants, Programming Languages, Verification, Computer Science

Project ideas

Project ideas are meant to help inspire student thinking about their own project. Students are in the driver seat of their research and are free to use any or none of the ideas shared by their mentors.

A Compiler for a Graph-Structured Functional Language

High-level programming languages typically use a tree-based representation of programs. For example, the expression "x + (y * 8)" is represented by a tree with "+" as the root, "x" as the left branch, and the tree representing "y * 8" as the right branch. On the other hand, low level code, like assembly or most compilers' intermediate representations, is represented by a control-flow graph, with blocks of code that can point to any other block of code in the program. Unlike with trees, graphs can contain loops, which allows them to directly represent recursion and looping constructs. This project focuses on designing a high-level language with a graph representation and exploring how the design influences compilation.

Verification of a Transitive Closure Algorithm

Graphs are structures made up of a set of vertices and edges between them. Many graph algorithms rely on the transitive closure of a graph, which adds a direct edge between two vertices whenever one is reachable from the other. This project focuses on implementing and proving correct a transitive closure algorithm that uses a technique called graph powering in the Coq proof assistant.

Coding skills

Coq, OCaml, Haskell, Racket, Java 8, Javascript, Python, C, Assembly

Interested in working with expert mentors like Dustin?

Apply now