Correctness of normalization-by-evaluation for STLC

quotient types in cubical Agda

Work in progress on semi-simplicial types

Denotational semantics based on graph and filter models

Multimode simple type theory as an Agda library.

An extension of the NbE algorithm to produce computational traces

Experiments with higher-order abstract syntax in Agda

formalization of an equivariant cartesian cubical set model of type theory

An agda library for developing synthetic category theory - and other synthetic mathematics

A formalization of System Fω in Agda

A formalization of the theory behind the mugen library

Meta-theory and normalization for Fitch-style modal lambda calculi

Linear Logic for Constructive Mathematics, in Agda

Simply-typed lambda calculus as a QIT in cubical Agda + normalization

An embedding of ZFC into Agda

https://metaborg.github.io/mj.agda/

Syng: A syntactic approach to concurrent separation logic with propositional ghost state, fully mechanized in Agda

Agda mechanisation of the University of Cambridge Semantics of Programming Languages course

Type theories as quotient inductive-inductive-recursive types

Some rudimentary proofs on subtyping

ModTT in Agda

Various attempts to model version control systems in Homotopy Type Theory

Agda formalization for the POPL 2026 paper "Di- is for Directed: First-Order Directed Type Theory via Dinaturality".

A Logical Relation for Martin-Löf Type Theory in Agda

Computational erasure as a SOGAT

[WIP] Orthogonal-Reflection Construction

An implementation of a first-order auto tactic for Agda, in Agda.

Self-studying for category theory with agda