Research

Broadly, I am interested in the design, semantics, and implementation programming language design and implementation wherein I focus on correctness and portability of techniques with regard to a language’s features. For instance, my PhD work focused on the promoting the implementation level feature of closures to a first class element of the compiler intermediate language with their own equational theory. Justification of this work involved realizability model over environment abstract machines wherein closures are manifest.

My current focus is on the definition of portability as a property that can be represented in the type. To date, portability of programs for different heterogeneous hardware is a vague notion without static guarantees.

Keywords compilers, abstract machines, realizability, verification

Writing

Zachary J. Sullivan. Reflections of Closures. University of Oregon. Dissertation. 2023. [doc]
Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. Closure Conversion in Little Pieces. International Symposium on Principles and Practice of Declarative Programming. 2023. [doc]
Zachary J. Sullivan. Deriving Practical Implementations of First-Class Functions. University of Oregon. Technical Report. 2021. [doc|slides]
Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. Strictly Capturing Non-strict Closures. Workshop on Partial Evaluation and Program Manipulation. 2021. [doc|slides]
Paul Downen, Zachary Sullivan, Zena Ariola, Simon Peyton Jones. Making a Faster Curry with Extensional Types. Haskell Symposium. 2019. [doc]
Zachary Sullivan. Exploring Codata: The Relationship to Object-Orientation. University of Oregon. Technical Report. 2019. [doc]
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. Codata in Action. European Symposium on Programming. 2019. [doc]
Zachary Sullivan. The Essence of Codata and Its Implementations. University of Oregon. Masters Thesis. 2018. [doc]

Software

The Dual Language and its compiler

Based on work found in my masters’s thesis, the DL language is a simple language with user-defined data and codata types. The language contains nested pattern and copattern matching. The DL compiler is a prototype compiler that supports compilation of codata types to several backends: Racket, Ocaml, JavaScript, and Haskell.

Haskell Codata Language Extension for GHC

This version of GHC adds a language extension {-# LANGUAGE Copatterns #-} that adds codata types and nested copattern matching to Haskell. It is based on work found in my masters’s thesis.

There is a repository of examples using this language extension. It includes codata versions of examples from John Hughes’s famous paper promoting on-demand programming: Why Functional Programming Matters.

Additionally, Emacs users might want to used this extension to haskell-mode, which includes support for the new syntax.

GHC Core Extended with Extensional Functions

A prototype implementation of Making a Faster Curry with Extensional Types can be found here. Once this compiler is built, the optimization can be enabled with the -feta-arity flag.