Andreas Abel

miniagda. A prototypical dependently typed languages with sized types and variances

strong-normalization. Formalizations of strong normalization proofs

helf. Haskell implementation of the Edinburgh Logical Framework

ipl. Agda formalization of Intuitionistic Propositional Logic

java-adt. A tool to create immutable algebraic data structures and visitors for Java (such as abstract syntax trees).

agda2lagda. Simple conversion from Agda text to literate Agda text.

haskell-style-guide. A style guide for Haskell code.

cabal-clean. Remove outdated compilation artefacts left by cabal v2-build

proposal-agda-tutorial. Proposal for an Agda tutorial

universal-algebra. Formalization of some universal algebra in Agda

agda-automata. Formalisation of automata in Agda

risc386. Interpreter for symbolic 386 assembler (small fragment) written in Haskell

shift-reset-dsl. A DSL for shift and reset in Agda

ObjTT. Haskell

Sit. Prototypical type checker for Type Theory with Sized Natural Numbers

sized-types. Stuff concerning sized types.

lambda-definability. Lambda-definability and NBE for simply-typed lambda-calculus and maybe beyond

type-preserving-cps. Type-preserving CPS translation for simply- and dependently-typed lambda calculi

lambda-pi. An implementation of Lambda-Pi in Agda