Harrisons's HoPLaAR

Lecture notes and problem sets for EECS 598 Category Theory

Experimental library for Narya

A verifier for automated and interactive proofs about transition systems.

comparative formalizations of the Yoneda lemma for 1-categories and infinity-categories

Tools for Generating and Exploring Agda's Definition and Module Dependency Graphs for Better Code Comprehension and Parallel Type-Checking

System benchmarking for proof assistants

Proof theory seminar

Intrinsic Verification of Formal Grammar Theory

A Lean4 Formalization of Polynomial Functors

Dependent Polynomials in Agda

Formal proofs related to coslice colimits and 2-coherent left adjoints

My Agda blog/lab/playground

Supplementary types and functions for the Agda prelude

Hefty inspired effects library for cubical-mini

A curated list of awesome qubes os links

A Mirage firewall VM for QubesOS

A linear algebra library using agda standard library

A list of works and resources about double category theory, with a particular focus on applications.

An Agda library for reasoning about asynchronous iterative algorithms and network routing problems

Formalisation of some ideas related to continuations and co-exponentials

Article on using refinement calculus and algebraic effects for parsing

A Philosophy of Math Education