Selected Software by Aaron Stump and Collaborators
Cedille is a new proof assistant based on a minimalistic impredicative constructive type theory.
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 220.127.116.11. 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.
An implementation called fore of F-omega plus positive-recursive global type definitions, in Agda (18.104.22.168),
here (updated May 19, 2015).
Versat, a statically verified SAT solver, as a single C source file, and as Guru source files: versat.zip. 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: guru-lang.zip.
Elementary definitions for domain theory, and a simple example, in Agda are
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: ocaml-smt2.zip (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. slothrop.zip. This is described in this paper.