projects

Certifying Typechecker for LF

A bidirectional typechecker for LF that uses normalisation by evaluation for equality checks and generates a declerative derivation tree as a certificate.

Public codebaase soon!

Racket-ish Compiler

An end-to-end compiler for a Racket-like language in Typed Racket with typed IRs and type preservation for those IRs.

The typed IR definitioons and some macros are here

Capability-Based Multikernel OS

A Barrelfish-inspired research OS on ARMv8-A.

I Can’t share this one :(

SQL-like Data Querying DSL

An extensible SQL-style query language for filtering and aggregating structured datasets.

I can’t share this one :(

Turing Machine Visualiser

A Haskell + GTK3 visualiser for Turing machines.

Codebase is here

SAT-Based Circuit Designer and Simulator

An extensible circuit simulator and visual editor built with Prolog, C, and GTK3.

I can’t share this one :(

Agentic Research Loop for Nonprofit Newsletters

An agentic research system on GCP that searches the web, evaluates source trustworthiness, and generates update newsletters and emails for nonprofit campaigns.

This is an industry project and I also wouldn’t want to share this one