Source code for my Master's Thesis

Matters of Call-by-value

Formalise ∞-monoids in two-level type theory

A proof assistant for higher-dimensional type theory

Code formatting and document conversion utilities for forester

experimental

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

TagTime online.

TeXpresso: live rendering and error reporting for LaTeX

Code repository for our work on Quantum Pi

Where we explore more interesting data types than just fixed points of polynomials

Agda code accompanying the SqrtPi paper

Cut-elimination by Semantic Means

Implementation in OCaml of a strong reduction machine for Intuitionistic Multiplicative Exponential Linear Logic (IMELL) that has linear overhead on the number of reduction steps and the size of th…

Using Forester, We are attempting to resurrect and grow the since deleted model theory wiki and give it a better foundation for future growth.

VSCode support for Forester

Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories

A digital archive of category theory papers.

Implementation of the lambda-lambda-bar calculus from "The Duality of Abstraction" https://vikraman.org/files/popl24-coexp.pdf

Quantum circuits compiler with staging and continuations

Procedure to change the SSID of the Vodafone Power Station

A Causal-Consistent Reversible Debugger for Erlang

A Causal-Consistent Reversible Debugger for Erlang

Mechanized Theory of Event Structures

A lightweight window border system for macOS