# 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).

## Links

^{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. ↩}