An introduction to programming language theory in Agda

The Agda standard library

An experimental library for Cubical Agda

A new Categories library for Agda

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

An introductory course to Homotopy Type Theory

Lecture notes on univalent foundations of mathematics with Agda

The theory of algebraic graphs formalised in Agda

A cost-aware logical framework, embedded in Agda.

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…

Congruence Closure Procedure in Cubical Agda

Formalization of Regular Languages in Agda: regular expressions, finite-state automata, proof of equivalence, proof of the pumping lemma.

Reversible programming in Agda

Files related to my paper "Continuity of Godel's system T functionals via effectful forcing". MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119-141.

Trace monoids in Cubical Agda

Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda

Formalisation of Church Rosser Theorem

a formalisation of the theory of pregoups as described by Lambek in Agda

Formalised complexity proof for "Efficient CHAD" in Agda