My team (Avery Blanchard, Jackie Ryu) and I implemeted an encrypted version of Facebook's <a href="https://engineering.fb.com/2013/06/25/core-data/tao-the-power-of-the-graph/">TAO</a> engine
for our final project for the graduate <a href="https://systems.cs.columbia.edu/private-systems-class/">Privacy-Preserving Systems</a> seminar at Columbia.
Facebook's TAO (The Association of Objects) is a data model and API tailored for serving the social graph, acting as a proxy over a SQL Database. At a high level, it translate graph queries into SQL queries to serve social graph data on a regular SQL database.
We implemented a simplified version of TAO (as a proxy server over a Postgres DB) with Rust. On top of that, we incorporate deterministic encryption and our own implementation of order-preserving encryption into TAO, such that every data stored in the backend DB is fully encrypted. With this, our TAO can serve graph queries on fully encrypted data (including range queries!).
Our code and presentation slides can be found in our <a href="https://github.com/encrypted-tao/encrypted-tao">github repo</a>!

Simplified Implementation of Facebook's TAO engine, plus encryption. In Rust.

Encrypted-TAO

My friend Andrei Coman and I implemented a session-typed pi calculus interpreter for Columbia's
graduate programming languages course (<a href="http://www.cs.columbia.edu/~sedwards/classes/2023/6998-spring-tlc/index.html">COMS 6998: Types, Languages, and Compilers</a>), taught by Prof. Stephen Edwards.
In particular, we implemented the type system studied in <a href="https://link.springer.com/article/10.1007/s00236-005-0177-z">"Subtyping for session types in the pi calculus"</a>
by Simon Gay and Malcolm Hole (2005).
The type system the correctness of a communication patterns in multi-threaded
pi-calculus programs with respect to its defined session type. We also implement a pi-calculus
evaluator that executes the given program, based on the operational semantics in the paper.
Below is an example of a pi-calculus program our interpreter can type-check and evaluate - not that it's readable in any way :^)
<pre><code>(v x : ^['[?{int, int}.!{int}.!{int}.end]])
 ((v y : '[?{int, int}.!{int}.!{int}.end])
 x![y].y![2, 3].y?[z : int].y?[w : int].zero
 |
 x?[y : '[?{int, int}.!{int}.!{int}.end]].
 y?[z : int, w : int].y![z].y![w].zero)
</code></pre>
Our interpreter is implemented with the OCaml language, and can be found in <a href="https://github.com/session-pi/session-pi">this github repo</a>! Our project write-up can be found in the <a href="http://www.cs.columbia.edu/~sedwards/classes/2023/6998-spring-tlc/reports/Session-report.pdf">course website</a>.

Session-Pi

I implemented pattern matching anomaly detection for <a href="https://github.com/ssm-lang/sslang">sslang</a>,
a programming langauge from <a href="http://www.cs.columbia.edu/~sedwards/index.html">Prof. Stephen Edwards's lab</a> at Columbia.
sslang is built upon the sparse synchronous model, supporting precise timing prescription and deterministic concurrency.
I implemented Luc Maranget (from INRIA)'s <a href="http://moscova.inria.fr/~maranget/papers/warn/warn.pdf">pattern matching anomlay detection algorithm</a>, in sslang's IR (with Haskell). This pipeline generates compiler warnings for non-exhaustive pattern matching, or useless arms. For instance, in sslang:
<pre><code>type List a
 Cons a (List a)
 Nil

-- Example 1:
f x =
 match x -- this pattern matching is not exhaustive
 Cons _ _ = 1

-- Example 2:
f x =
 match x
 Nil = 0
 Cons _ Nil = 1
 Cons _ l = 2
 Cons _ _ = 3 -- this arm is useless!
</code></pre>

Detecting useless arms in, or non-exhaustive, pattern matching in the sslang language

Pattern Matching Anomaly Detection in sslang

For <a href="https://verigu.github.io/4115Fall2022/">Columbia's compilers course</a>, my group (Andrei Coman, Scott Geng, Alan Zhao, Eumin Hong) and I
built Orlang, a functional programming language targetting the LLVM IR. The compiler is written in the OCaml langauge.
Orlang is syntactically similar to OCaml, with strict evaluation, a strong, static, and polymorphic type system based on the Damas-Hindley-Milner
type system. Orlang also supports higher-order functions, currying, recursion, and some built-in list functionalities.
Below is a cool Orlang program, featuring pattern matching, list functionalities, recursive let-bindings, and currying!
<pre><code>let applyFnList flist alist =
 let rec applyHelper fs as acc =
 match |.fs.| with
 | 0 => reverse acc
 | otherwise => let (f::ff) = fs in
 let (a::aa) = as in
 applyHelper ff aa ((f a)::acc)
 ;
 in applyHelper flist alist []

val fnList : List (Int -> Int -> Int)
let fnList =
 [add, subtract, multiply]
 where add = (\x y -> x + y)
 and subtract = (\x y -> x - y)
 and multiply = (\x y -> x * y)

val print_list : List Int -> List ()
let print_list lst = map (\x -> print (extend (string_of_int x) [' '])) lst

val main : ()
let main =
 let lst1 = [1, 2, 3] in
 let lst2 = [4, 5, 6] in
 let curried = applyFnList fnList lst1 in
 let res = applyFnList curried lst2 in
 let pnt = print_list res
 in ()
</code></pre>
Find Orlang in <a href="https://github.com/orlang-proj/orlang">this github repo</a>!

Orlang

I wrote a reinforcement learning agents framework back in high school, when when I was
interested in RL/ML (still interested, but not as much!). I wrote modular implementations
of the state-of-the-art RL algorithms back then (~2019/2020, so think Rainbow-DQN, Soft Actor Critic, etc).
The algorithms implemented are: DQN variants (DDQN, C51, QR-DQN, Rainbow, +Noisy Networks, +Prioritized Exp Replay);
A2C and A3C; original DDPG and Fujimoto's DDPG; and Soft Actor Critic. I've also implemented distributed training (Ape-X),
but in a <a href="https://github.com/cyoon1729/distributedRL">different repo</a>.
This project is no longer maintained, but here's the <a href="https://github.com/cyoon1729/RLcycle">github repo</a>. It was somewhat popular
when it was being actively maintained :) - had about ~270 stars and ~50 forks!

Modular Reinforcement Learning Agents Framework

Encrypted-TAO

Session-Pi

Pattern Matching Anomaly Detection in sslang

Orlang

RLCycle