cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Formalization of Mathematical Logic

string diagram editor

Godot Engine – Multi-platform 2D and 3D game engine

Lean4 library for substitution inspired by autosubst

Lean4 library for indexed inductive container types (i.e., Vec)

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization

An ott-like DSL embedded in Lean.

Compile Lustre to C

Towards generic type checking implementations in Haskell via second-order abstract syntax.

Library for building agents and managing LLM interactions

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