Turn .sql files into virtual-statements.

A small lense library for Racket.

Mechanizations of Type Theories

Public hosting for bain-cs111 webpage.

Distributions of Agda executable compiled into WebAssembly.

Style definitions for nice terminal layouts 👄

papers of Per Martin Löf

Linear algebra formalization in Agda

Experiments with guarded recursion

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

formalization of an equivariant cartesian cubical set model of type theory

A polynomial model of a Martin-Löf type theory a bit of game semantics

antifunext

A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.

Extensions to the cubical stdlib category theory for categorical logic/type theory

Haskell Functional Reactive Programming framework with type-level clocks

Experimental implementation of a Cubical Type Theory modeled by presheaves over posets

Literate Drag and Drop Using the Racket GUI

A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.

ICFP 2024 artifact

A massively parallel, high-level programming language

A massively parallel, optimal functional runtime in Rust

A work-in-progress core language for Agda, in Agda

Cosette is an automated SQL solver.

Experimenting on ornamentation in Agda via reflection.

The original sources of MS-DOS 1.25, 2.0, and 4.0 for reference purposes

A minimal GPU design in Verilog to learn how GPUs work from the ground up

A lightweight dynamic instrumentation library

A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"

Lecture notes and exercises for the advanced course on categorical realizability at the Midlands Graduate School (MGS) 2024