Ulf Norell

agda-prelude. Programming library for Agda

insane. Toy typechecker for Insanely Dependent Types

x86-agda. Inline, type safe X86-64 assembly programming in Agda

agda-summer-school. Summer school on programming in Agda

agda-bench. Benchmarking tool for compile-time performance of Agda programs

quasi-quote. Quasi-quoting library for agda

category-theory-experiments. Agda

effects. Porting the Idris Effects library to Agda

curves. Haskell library for drawing pretty pictures

aim23-talk. Agda

agda-cufp. CUFP tutorial 2014

agda-tactics. Agda

aim-xl-talk. Sound and complete validators (AIM XL talk)

version. Utility program for version switching

categories. Categories parametrized by morphism equality, in Agda

agda-nofib. Benchmark programs for Agda

me-em. Model Examples, Example Models

agda-readline. Bindings to editline

agda-logo.