An introduction to programming language theory in Agda

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

An introductory course to Homotopy Type Theory

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

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

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Inline, type safe X86-64 assembly programming in Agda

Refinement types + dependent types = ❤️

Where my everyday research happens

A Brainfuck interpreter written in Agda

being bits and pieces I'm inclined to leave lying around

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

A library and case-study for linear, intrinsically-typed interpreters in Agda

Work in progress

Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/)

mechanization paired with https://github.com/hazelgrove/hazelnut-dynamics

A categorical semantics library in Agda.

A tiny compiler for a security-typed imperative language with a formalised proof of noninterference-preservation.

Agda code for experimenting with internal models of cubical type theory

Contextual Modal Type Theory, formalization and implementation

Library for generic programming with context-free elements in Agda