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 (also we have one for 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:

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.