An introduction to programming language theory in Agda

Lecture notes on univalent foundations of mathematics with Agda

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

Agda formalisation of second-order abstract syntax

antifunext