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

Coq library for rose trees

The Fan theorem for inductive bars and a constructive variant of König's lemma

Kruskal and Higman type tree theorems for the Kruskal-AlmostFull library

Library of basic results about Almost Full relations in Coq

A work-in-progress core language for Agda, in Agda

FAQ about Madrid for digital nomads