Altan Haan

Hello there! This is my professional homepage, where you can find information about me, my current projects, research, and so on.

About

I am currently a 3rd year (i.e. junior) undergraduate studying in the Allen School at the UW, where I am majoring in computer science. I am also a math major. I enjoy broadly the areas of programming languages, formal methods (in particular program synthesis and verification), and category theory. My hobbies include (but are not limited to) gaming, chess, and discovering new music.

Research

Areas of interest: programming languages, formal methods, program synthesis, program verification, type theory, category theory, compilers, theory of computation, architecture.1

Analysis of CDCL Program Synthesis. I am currently finishing up an exploratory research project with James Bornholt on Program Synthesis using Conflict-Driven Learning. In particular, we are trying to concretely understand why this CDCL-based synthesis algorithm performs well, by analyzing the lemmas generated by the conflict-learning step. To do this, I wrote an implementation of the paper's core algorithm in Rosette, a solver aided language that naturally embeds an SMT solver (along with its primitives) into Racket. Using this implementation, we plan on analyzing the conflict lemmas for interesting properties that correlate with synthesis success.

Colocolo. As the class project for CSE 507, I am working with Thomas Bernardi on building a relational logic solver we call Colocolo.2 This solver will be written in Rosette, and based heavily off of James's Ocelot solver. It will be primarily an optimization: we aim to implement (1) skolemization, (2) an optimized SAT solver backend (along with optimal CNF-SAT formula transformations), and (3) symmetry breaking, the last of which was attempted by Ocelot but mysteriously caused performance problems.

TVM/Relay. I am currently in talks with Jared Roesch on working on the TVM deep learning compiler stack. In particular, I am interested in the high-level IR language Relay used by TVM to represent tensor programs. Relay provides a high level interface to the rest of the TVM stack, performing various graph-level and even program-level (with the inclusion of constructs like recursion) optimizations. Relay's type system is of particular interest, as it deals with tensor shapes in order to facilitate aggressive lower-level optimizations.

Projects

Under construction.

Selected Coursework

CSE. Computer-Aided Reasoning for Software (507); Operating Systems (451); Data Structures and Parallelism (332); Systems Programming (333); Hardware/Software Interface (351); Software Design and Implementation (331); Logic and Discrete Math (311, 312).

MATH. Honors Calculus I (134, 135, 136); Honors Calculus II (334, 335, 336); Ring Theory (402); Topology (441).

1. These areas are listed approximately in order of interest, but this is hard to quantify and frequent to change. Also, some of the listed areas are subareas of others - this is due to my interests still very broad, so I expect this to change with time.
2. A colocolo is a "small wild cat native to South America." We chose this name to follow in the style of Ocelot, which was a reference to Kodkod, a state-of-the-art relational logic solver.