Selected Software by Aaron Stump and Collaborators
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.
Over the past seven years I have developed the Guru programming language, which features full-spectrum dependent types.
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.