Intrinsic Verification of Formal Grammar Theory

being the programs and code for a paper about general recursion

Dependently typed Algorithm M and friends

Correctness of normalization-by-evaluation for STLC

quotient types in cubical Agda

being the introduction to co-de-Bruijn metasyntax

Interactive and object-oriented programming in Agda using coinductive types

Tic Tac Toe, formalized in Agda

A dependently typed type checker for a TT with intervals

Formalization of type theory

Simply typed lambda calculus in cubical agda

mechanization paired with https://github.com/hazelgrove/hazelnut-dynamics

Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.

AACMM's generic-syntax, but with QTT-style annotations

Agda formalisation of dual-context constructive modal logics.

A formalization of the theory behind the mugen library

Type-preserving CPS translation for simply- and dependently-typed lambda calculi

Hacking synthetic Tait computability into Agda. Example: canonicity for MLTT.

A formalization of System Fω in Agda

An Agda library for programming with ternary relations

Quasi-quoting library for agda

A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.

A categorical semantics library in Agda.

A tiny compiler for a security-typed imperative language with a formalised proof of noninterference-preservation.

Agda suffices: software written from A to Z in Agda

Experiments in Synthetic Differential Geometry

being the emperor of Mongo, but also a verb

Machine-checked Agda formalization for the ILC project