System F-omega normalization by hereditary substitution in Agda

Learn the Agda basics in three 2-hour sessions.

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

The Spire Programming Language

A formalization of category theory in cubical Agda

Minimalistic dependent type theory with syntactic metaprogramming

Observational Type Theory as an Agda library

Agda formalisation of second-order abstract syntax

Where my everyday research happens

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

being bits and pieces I'm inclined to leave lying around

Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages.

being the materials for a paper I have in mind to write about the bidirectional discipline

Like "Write Yourself a Scheme in 48 Hours", but in Agda

A TACtic library for Agda

Showing how some simple mathematical theories naturally give rise to some common data-structures

Porting of software foundations book to Agda

Paradoxes of type theory, described didactically. With accompanying proofs in Agda.

Work in progress

The Agda Universal Algebra Library (html docs available at the url below)

IO using sized types and copatterns

A library and case-study for linear, intrinsically-typed interpreters in Agda

Constructive Galois connections

A toy dependent typed language.

A polynomial model of a Martin-Löf type theory + a bit of game semantics

Mechanizations of Type Theories

Self-contained repository for the eponymous paper

Formalised embedding of an imperative language with effect system into session-typed pi calculus.

Mtac in Agda

A formalization of Pure Type Systems (PTS) in Agda