Senior Thesis Research
In my senior year I worked on a methodology for verifying the
correctness of a compiler phase, in this case specifically closure
conversion. To do this I created a shared language that combines
the source and target languages together, allowing source and target
programs to be meaningfully compared to one another. To do this
comparison I used contextual equivalence, which effectively says
that two programs are equivalent if no matter how they are used
they cannot be differentiated. Thus I proved that the compiler
compiles the source program to an equivalent target program, so
that the two behave the same, which verifies correctness. You can
view my poster on my thesis here,
as well as my full thesis here.
Independent Study Research
In my junior year I did an independent study where I implemented a
static verification checker for the language
C0. I used the
Z3 theorem prover to actually
perform the analysis of checking certain conditions given certain
facts. The tool I created checks for many errors, including array
index-out-of-bounds accesses, null pointer dereferences, arithmetic
errors (like division by zero). It does this by making use of the
languages contracts, which are statements that make guarantees
about variables while inside loops and when entering or leaving a
function. You can view my poster on my work
here.
C0 Compiler
In my Compiler Design course (15-411), I wrote a full compiler for
the language C0 with a
partner. The compiler takes C0 programs and compiles them into
x86-64 assembly, which is linked to a runtime system. The runtime
also has a mark-and-copy garbage collector that is integrated into
the code if used. It also has an implementation of our semantics
for having free in C0 (while still being defined in all
cases). I primarily worked on the parser, elaboration, typechecking,
and translation (as well as parts of the garbage collector). We
plan to continue development on it in our spare time.
Dynamic Memory Allocator (Malloc)
Also for my Introduction to Computer Systems course (15-123), I
wrote a dynamic memory allocator in C. I implemented it as a
segregated free list for performance, and tried to minimize the
amount of extra space used for each block by making efficient use
of bits. Code available upon request (which contains an in depth
explanation of how the allocator works).
Project Lucid
As a part of the Game Creation Society (GCS) at Carnige Mellon, I
worked on a team to complete the game Lucid, a sidescrolling 2d
platformer/shooter written in Actionscript. I focused on
developing some of the physics, as well as level interpretation.
You can find out more and download it
here.
Mandelbrot Set Generator
As a challenge in my Principles of Functional Programming class,
I wrote a program for displaying something that would be
considered art. Since simply displaying a hard-coded piece of ascii
art is boring, I decided to make a fractal generator (specifically
the Mandelbrot Set). I made it in SML, and can be run by entering
"whatisart()" in the REPL (like with
SMLNJ) after using the file.
The code can be found here.