Staged compilation with dependent types

Haskell implementation of a version of cubical type theory developed for my master thesis

Emacs support library for PDF files.

A website containing a bibliography for non-well-founded and cyclic proof theory

Implementations of various type systems in OCaml.

A Proof-oriented Programming Language

A Dependently Timed Drum Machine Language

A slightly more Glorious Haskell Compiler

Minimal implementations for dependent type checking and elaboration

Lecture notes on realizability

Hedy is a gradual programming language to teach children programming. Gradual languages use different language levels, where each level adds new concepts and syntactic complexity. At the end of the…

Prototype implementation of the bidirectional instances extension for Haskell

Literature review of GHC's Core language, System FC

Proposed compiler and language changes for GHC and GHC/Haskell

Lambda normalization and conversion checking benchmarks for various implementations

A collection of useful .gitignore templates

Introduction to algebraic effects and handlers

Bare metal experiments using LC and mil-tools

Lightning is a Java based, super fast, multi-mode, asynchronous, and distributed URL execution engine from eBay

Programming Language Theory λΠ

A web server written in Coq.

Richard A. Eisenberg's PhD Dissertation

A textbook on informal homotopy type theory

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Experiments wring interpreters with Haskell.

Algorithms, 4th edition textbook code and libraries

Interview questions

Shared server-based space for A-Frame scenes.

Programming in Haskell by Graham Hutton