Test cases for Writing a C Compiler

Aeneas tutorial for ICFP

Artifact for the Functional Pearl "Grokking the Sequent Calculus"

A proof assistant and a dependently-typed language

Subtyping calculus of inductive constructions

audit your cabal projects for haskell-specific security-advisories

Changes and Pinafore projects. Pull requests not accepted.

Mutation analysis library for haskell

Experimental proof assistant (and architecture) for dependent linear logic

Preprocessor for typesetting Haskell sources with LaTeX

Pattern matching and exhaustiveness checking algorithms implemented in Rust

Fast equality saturation in Haskell

Fast equality saturation in Haskell

Accessing tuple fields in Haskell using record dot syntax.

The Helium compiler, Helium-as-a-library, and the texthint interpreter

Hand-curated bibliography for my projects.

A Language with Dependent Data and Codata Types

Comonoid trait for Rust.

The Pointer Abstract Machine from Sec. 9 of Curien & Herbelin's "The Duality of Computation"

Duo - A research language exploring duality in programming language design

A community-driven collection of documentation for Haskell error messages and warnings

Chapelure is a diagnostic library for Haskell

Official repository of the Autosubst 2 project.

Repository accompanying the ZuriHac Advanced Track lecture on Datatype-Generic Programming

Haskell library for the Microsoft Language Server Protocol

Create Vega-Lite visualizations from Haskell.