- ROSCoq :
- CFGV : If you are interested formalizing (some properties of) a language with variable bindings, this Coq framework might give you a headstart. It is parameterized meta-theory with ready-to-use definitions of simultaneous substitution, alpha equality, freevariables, e.t.c. and many proofs about them. You can use them by instantiating our meta-thory with its parameter, which is of the type CFGV. CFGV is a record type which lets you specify a language as a Context Free Grammar but with some additional information about Variable bindings.
- Coq Query Server : If you have large Coq developments and want the readers (e.g. of your associated paper) to be able to lookup the definitions by name without having to manually find it in the large collection of .v files, this tiny webserver might be useful. I originally wrote it to enable the help the reviewers of our ITP 2014 paper lookup definitions of concepts that were mentioned in the paper, but whose full definitions were omitted from the paper due to space constraints. This server communicates with coqtop and lets the user issue queries like Check , SearchAbout , SearchPattern , About , Print and Print Assumptions . An instance of this server can handle multiple Coq projects.
- nbcoq : A Coq plugin for the Netbeans IDE. Features include coqdoc-like syntax highlighting, latex to unicode conversion, experimental support for jumping to definition, an elaborate mechanism to issue queries like the ones mentioned above, bunching of hypotheses of same type.
