An introduction to programming language theory in Agda

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

Total Parser Combinators in Agda

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

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

A formalization of category theory in cubical Agda

A self-contained repository for the paper Type and Scope Preserving Semantics

Semantics of Programming Languages