Experiments with preordered set models of (directed) type theories

algebraic typechecking and elaboration of type systems

Relational algebra implementation in Agda with simple bindings to SQLITE

Various mechanized proof files for fun.

Type Theory in Type Theory using Cubical Agda

Dealing with Flags and Options

My Agda blog/lab/playground

Experiments with effect systems

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

A well typed interpreter for the simply-typed lambda calculus written in Agda

Functional Linear Algebra with Block Matrices

Some rudimentary proofs on subtyping

numbers as quotient types

Using lambda calculus as the syntax for cartesian closed categories, ala Conal Elliott.

Constructing Simple and Mutual Inductive Types in Agda.

Mechanized formalization of Implicit resolution in Agda

An Agda formalisation accompanying the examples given in Section 7 of the paper "Handling fibred algebraic effects".

"Software Foundations" Agda challenge

mechanization for livelits paper, https://github.com/hazelgrove/livelits-paper

Coinductive Formalization of SECD Machine in Agda

Master's thesis project: A refactoring engine for Agda. Very much under construction.

Nils Anders Danielsson's Total Parser Combinators (mirror)

An Agda encoding of the primitive imperative language IMP from Glynn Winskel's ‘The Formal Semantics of Programming Languages’.

An executable formal semantics of Agda in K

Generating Library definitions from Theory Expressions