An introduction to programming language theory in Agda

The Agda standard library

An experimental library for Cubical Agda

Development of homotopy type theory in Agda

A new Categories library for Agda

An introductory course to Homotopy Type Theory

The agda-unimath library

Logical manifestations of topological concepts, and other things, via the univalent point of view.

Lecture notes on univalent foundations of mathematics with Agda

Compiling Agda code to readable Haskell

Programming library for Agda

Total Parser Combinators in Agda

A cost-aware logical framework, embedded in Agda.

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Cartesian Cubical Type Theory

Miller/pattern unification in Agda

Where my everyday research happens

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

Agda formalisation of second-order abstract syntax

The Iowa Agda Library

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

A TACtic library for Agda

H.O.T.T. using rewriting in Agda

Proof automation – for Agda, in Agda.

An implementation of Functional Reactive Programming

antifunext

IO using sized types and copatterns

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

A Unifying Cartesian Cubical Set Model

Mechanizations of Type Theories