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.