An introduction to programming language theory in Agda

The Agda standard library

An experimental library for Cubical Agda

A new Categories library for Agda

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

Total Parser Combinators in Agda

Agda formalisation of the Introduction to Homotopy Type Theory

A slow-paced introduction to reflection in Agda. ---Tactics!

Agda bindings to SMT-LIB2 compatible solvers.

Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

A formalization of the polymorphic lambda calculus extended with iso-recursive types

A cost-aware logical framework, embedded in Agda.

Refinement types + dependent types = ❤️

The Spire Programming Language

A formalization of category theory in cubical Agda

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

Minimalistic dependent type theory with syntactic metaprogramming

being the teaching materials and exercises for CS410 in the 2018/19 session

Observational Type Theory as an Agda library

Agda formalisation of second-order abstract syntax

Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

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

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

The Evolution of a Typechecker

A TACtic library for Agda

The Iowa Agda Library