An experiment to see what interpretation into (pre)sheaves categories look like

A Pacman implementation in Rocq, extracted to C++ via Crane.

Framework for type-safe pure functional and non-cubical tensor processing, written in Idris 2

Monoidal categories in Agda

Dependent Lens FRP and concurrent model in Agda

Congruence Closure Procedure in Cubical Agda

Formalizing the Intel 4004 microprocessor

Lectures on Algebraic and Semi-Algebraic Reasoning for Formal Methods : IMDEA Madrid -- July 2025.

Functions and proofs about game trees in Rocq, implemented as rose trees.

An implementation of Dung's argumentation frameworks

Rust implementation of LT-PDR

an implementation of the Maurer Machine, as described in "Compiler Design: Virtual Machines" by Wilhelm and Seidl

toy implementation of Hindley-Milner type system that prints out inference steps

A well typed by construction kernel language for bidirectional programming

Functional implementation of anti-unification algorithm for multiple terms

A toy dependent typed language.

(Mirror) Implementation of the ONS (Ordered Nominal Sets) library in Haskell

Agda implementation of McBride's "First-order unification by structural recursion" paper

Mechanized proofs and example programs for the paper Type Inference Logics, published at OOPSLA24.

A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

Quasi morphisms for Almost Full relations