Software Contributions

OCaml / OCaml related

• odoc_xref.ml - custom ocamldoc html generator with the capability to cross-reference material from libraries: [odoc_xref.ml for 4.00] [odoc_xref.ml for 3.12]
• odoc_check.ml - custom ocamldoc module to check for missing documentation items and tags [odoc_check.ml for 4.00] [odoc_check.ml for 3.12]
• otags III - generate tags for emacs or vi[m] from ocaml sources
• Enhanced OCaml Documentation

Coq and Proof General

• Formalization of Coalgebraic Logics in Coq: documentation and sources
• Proof tree visualization with prooftree
• Adding multiple file support to Coq Proof General.
• coqgraph.ml is a simple tool for generating dependency graph's for Coq projects. Documentation and installation instructions are in the source file.
  Example dependency graphs:
  • my formalization of cut elimination: [JPEG] [PDF]
  • the 8.4 standard library: [JPEG] [PDF]

Other software related stuff

• GTK tutorial on catching Unix-signals
• user specific smarthost exim4 configuration on Debian etch and Debian Lenny
• Selected java card documentation
• pvs-status-smiley: Emacs lisp code to annotate PVS sources with proof status smilies

Legacy Stuff

The following links to stuff that was once hot, but has been unmaintained for several years now.

• Debian etch on a HP Compaq nc6320    
• Olmar - connect the Elkhound/Elsa C++ parser with OCaml
• Memcheck - runtime typechecking for OCaml
• Camlp5 undocumented features and Quotations in original syntax for Camlp5 and OCaml 3.09

Home Teaching Science Software Miscellaneous