Learn you an Agda (and achieve enlightenment)

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

Compiling Agda code to readable Haskell

Agda bindings to SMT-LIB2 compatible solvers.

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

ECMAScript back end for Functional Reactive Programming in Agda

Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

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

being the materials for CS410 Advanced Functional Programming in the 2014-15 session

Minimalistic dependent type theory with syntactic metaprogramming

Companion code for "Why Dependent Types Matter" paper.

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

being the materials for a paper I have in mind to write about the bidirectional discipline

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

A Brainfuck interpreter written in Agda

Cryptographic Constructions in the Type Theory of Agda

A TACtic library for Agda

Proof automation – for Agda, in Agda.

An implementation of Functional Reactive Programming

Paradoxes of type theory, described didactically. With accompanying proofs in Agda.

Porting of software foundations book to Agda

being a collection of Agda-facilitated ramblings

Deciding Presburger arithmetic in agda

Self-contained repository for the eponymous paper

Mtac in Agda

A formalization of Pure Type Systems (PTS) in Agda

Logical relations proof in Agda

Dependently typed Algorithm M and friends

wherein I implement several substructural logics in Agda

Dependently Typed Metaprogramming Exercises