Selected Software by Aaron Stump and Collaborators


The Iowa Agda Library is available via subversion from (username and password both "guest" without the quotes).

An implementation called fore of F-omega plus positive-recursive global type definitions, in Agda (, here (updated May 19, 2015).

Windows MSI to install Agda (2.5.2 installer had a problem and we will put it up when this is fixed). This will install Haskell, Agda, extra fonts for Unicode characters, and emacs. The MSIs are here (thanks to Brian Bacher). Restart your machine after installing the MSI in order to get your PATH variable set correctly for Agda.


Versat, a statically verified SAT solver, as a single C source file, and as Guru source files: Thanks to Mathias Fleury for pointing out that with recent versions of gcc, you will need to use something like this command-line to compile versat:

gcc -m32 -std=gnu89 versat.c.

Guru, a dependently typed programming language with imperative features via linear types; the Java source files are here:

Elementary definitions for domain theory, and a simple example, in Agda are here.

I am a co-developer of the gt grammar tool (main developer JJ Meyer). This is a frontend to the OCaml lex and yacc tools. From a single grammar file, you get OCaml lex and yacc files which parse input to (currently a little cluttered) syntax trees.

An OCaml parser for SMT-LIB format version 2.0: (5.5 MB).

Some large LF proofs: large_lf_proofs.tgz (5.5 MB).

The Archon interpreter and examples: archon.tgz. Archon is a meta-programming language, described more here.

The slothrop tool, by Ian Wehrman. This is described in this paper.