The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

Hacking on code from the paper "A simple type-theoretic language: Mini-TT" by Coquand et al.

Staged compilation with dependent types

Demo for high-performance type theory elaboration

This is a Coq formalization of Damas-Milner type system and its algorithm W.

typing haskell in haskell

Benchmarks for capture-avoiding substitution

Caml interpreter written in Haskell

Agda formalisation of NbE for λ□

A self-paced course to learn Rust, one exercise at a time.

A formatter for Haskell source code

A fourk of ormolu that uses four space indentation and allows arbitrary configuration. Don't like it? PRs welcome!

Companion code for llvm tutorial

Modeling and Proving in Computational Type Theory

bidirectional type checking algorithms for higher-ranked polymorphism

Essentials of Programming Languages in Haskell

EOPL in Haskell

Exercises for EOPL in Haskell

A modular happy extension providing a recursive ascent-descent backend

Text and Haskell source for my blog series on recursion schemes.

papers of Per Martin Löf

Demo for dependent types + runtime code generation

Kaleidoscope Tutorial using llvm-hs

Repository with code snippets that accompany episodes of The Haskell Unfolder

3D rubik_cube in LEAN

Research language for array processing in the Haskell/ML family

A demo implementation of a simple dependently-typed language

Lox language interpreter written in Rust

Toy language to show the conversion of embedded higher-order abstract syntax (HOAS)