An introduction to programming language theory in Agda

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

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

Total Parser Combinators in Agda

A workshop on learning Agda with minimal prerequisites.

Refinement types + dependent types = ❤️

Learn the Agda basics in three 2-hour sessions.

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

Like "Write Yourself a Scheme in 48 Hours", but in Agda

being the materials for CS410 Advanced Functional Programming in the 2015/16 session

A formalization of M-types in Agda

A library for doing generic programming in Agda

Implementing grep in Agda

An Agda formalization of System F and the Brown-Palsberg self-interpreter

being the introduction to co-de-Bruijn metasyntax

being the emperor of Mongo, but also a verb

Grimoire of Alice

Exercises from "Dependent Types at Work"

A monadic translation of Gödel's System T in the spirit of Gentzen's negative translation

Reading along with Types And Programming Languages

Stuff about the simply typed lambda calculus