Selected Software by Aaron Stump and Collaborators


DCS, a pure functional language where termination of all functions is enforced by typing. Subtyping plays a crucial role.

The Iowa Agda Library, recent versions, is available on github. Older versions can be found via subversion here (username and password both "guest" without the quotes).

Windows MSIs to install some recent versions of Agda. The most recent is The MSIs will install Haskell, Agda, extra fonts for Unicode characters, and emacs. The MSIs were created by U. Iowa IT support consultant Brian Bacher. Restart your machine after installing the MSI in order to get your PATH variable set correctly for Agda.


Cedille, a proof assistant based on a minimalistic impredicative constructive type theory.

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

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.

A solution in Coq using named variables, to the POPLmark challenge.