The Agda standard library

Agda bindings to SMT-LIB2 compatible solvers.

Miller/pattern unification in Agda

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

A TACtic library for Agda

A fast, easy-to-use ring solver for agda with step-by-step solutions

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

being a collection of Agda-facilitated ramblings

Deciding Presburger arithmetic in agda

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

Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories

what I did on my holidays

Agda sources used in my paper with Valeria de Paiva

being the teaching materials and exercises for CS410 in the 2020/21 session

Miscellaneous experiments in Aga

Reproducing results in papers to understand them.

Repository for my experimentation project with AutoInAgda