Dustin

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.