Python, Flask, PostgreSQL, SQLite, ElasticSearch, lots of internal tools
Habanero Lab at Georgia Tech alongside Prof. Vivek Sarkar and Dr. Caleb Voss. We investigated a language designed to statically detect certain bugs in promise-based programs. For example, our language guarantees that a promise can never be fulfilled twice and that the programmer cannot ever forget to fulfill the promise. This has some far-reaching effects: it's able to detect many common bugs that result from incorrect use of promises, it ensures that promises are used consistently (i.e. there's never a race to fulfill a promise), and it allows for easy instrumentation to dynamically detect deadlocks. This is all accomplished using a linear type system, in which promises are split into read handles and write handles (think promise vs. future in C++). The language consists of a simple concurrent programming language built on top of Java and utilizes promises as it's core concurrency primitive. A simple compiler (complete with a type checker, small runtime, and Java code generation) has been implemented in OCaml. We also defined a formal operational semantics for the language and used it to prove the guarantees of the language. (I also got to play around with the Coq proof assistant, though found it too tedious for a few of the proofs). I'm glad to announce that this work will be published at ECOOP 2021 as "Linear Promises: Towards Safer Concurrent Programming"! Huge thanks to my co-authors/mentors Caleb and Vivek!
OCaml, Coq, LaTeX, Java, Type Theory
Rust, ARMv8/aarch64 assembly, Raspberry Pi
FPGA SRAM interfaceAs our final project for my Digital Design Lab (ECE2031), we were tasked with designing and implementing an SRAM interface for a simple computer on an Altera DE2 FPGA. Optimizing for performance, we chose to create a device with qword addressability, which enabled users to take advantage of spatial locality by performing multiple loads/stores simultaneously. We also clocked our interface asychronously from the CPU, which allowed us to communicate with the SRAM between CPU clock cycles. While not the most technically complex project on here, this project really helped me learn more about VHDL and FPGAs in general.
Altera FPGAs (DE2), VHDL, SRAM, Quartus, Logic Analyzers, Oscilloscopes
Optimizing Tiger CompilerIn my compilers class (CS4240), we completed a toy compiler for the Tiger programming language. Using OCaml, our team developed a complete middle-end and backend for the MIPS-32 architecture. Heavily utilizing dataflow analyses, the compiler featured deadcode elimination, copy propogation, and Chaitin-Briggs register allocation. Best of all, I got the chance to finally use Nanocaml in a real project!
OCaml, Nanocaml (Nanopass), OCamlGraph, MIPS-32, Dataflow Analysis
Pipelined Processor DatapathFor my Systems & Networks class (CS2200), we designed a number of datapaths for a RISC computer based on MIPS. We individually designed a simple datapath for this computer in a logic simulator called "CircuitSim", then built on top of it to add interrupts and support for external I/O devices. As an extra credit project, I created a 5-stage pipeline version of the computer, which supported data forwarding and flushing the pipeline in order to resolve various hazards.
CircuitSim (logic simulator), "LC-2200" ISA
C, GBA BIOS
Bryan Phelps, and I'm one of many collaborators for the project.
Pierre-Malo Deniélou's and Nobuko Yoshida's research into global session type synthesis. The language itself is based loosely on Ruby and Elixir and compiles to Erlang code, but is designed around a new paradigm for actor programming using first-class session objects.
OCaml, Erlang/BEAM VM, Multiparty Session Types
Zach Baylin. Together, the three of began implementing a website for managing off-campus students' attendance. This quickly evolved into a full-fledged app, complete with user-customizable dashboards to view metrics about student performance, a route manager for teachers travelling between job locations, and tools for employers to evaluate students' performance. The latest revision of the web app is written in Crystal (using Kemal) and ReasonML (using ReasonReact), while the mobile app is written in Flutter.
Crystal, Kemal, ReasonML, React, Python, Qt, Ruby, Sinatra, Flutter, Dart, Postgres, GCP
Milo Turner and I whipped up a quick prototype of what such a library could look like. Though not yet battle-tested, this library provides a number of powerful abstractions for writing compilers quickly and easily.
OCaml, Nanopass Compilers, PPX preprocessors
KesefOver the summer of 2018, I became very interested in learning about finance. As part of this, I spent quite some time learning about financial statements such as those found in the 10-k/q SEC filings. To make browsing these forms easier, I used Perl6 to create a program called Kesef, which used a web scraper and RSS feeds to create a database of company filings. I also added some more features, such as rudimentary parsing of the XBRL documents to create tables of financial data and sourcing trading information from the IEX Trading API.
Perl6, XML (XPath, XQuery, and XSLT), IEX API
Zach Baylin and Eric Miller. For the competition, we were tasked with creating an app for browsing and checking out library books. After a failed first attempt using the Jasonette framework, we switched to Flutter (and fell in love with it!). The backend of the app was implemented in Ruby using Sinatra and PostgreSQL.
Flutter, Dart, Ruby, Sinatra, PostgreSQL