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 formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

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

An introductory course to Homotopy Type Theory

Learn you an Agda (and achieve enlightenment)

The agda-unimath library

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

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde

Lecture notes on univalent foundations of mathematics with Agda

Categories parametrized by morphism equality, in Agda

ECMAScript back end for Functional Reactive Programming in Agda

A workshop on learning Agda with minimal prerequisites.

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

Organization and planning for the Initial Types Club

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

Cartesian Cubical Type Theory

A cost-aware logical framework, embedded in Agda.

Summer school on programming in Agda

Learn the Agda basics in three 2-hour sessions.

A formalization of category theory in cubical Agda

Observational Type Theory as an Agda library

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

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

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

Cryptographic Constructions in the Type Theory of Agda

Modeling Ancient Greek Grammar