Available software from Yves Bertot

Tools around Coq

Packages for the Coq system

• A debugger for compound tactics,
• An elaborate search command,
• A local simplification tactic,

Graphical User-interface tools

• The CtCoq system.
• The pcoq system.
• graph representation of Coq data (in collaboration with Olivier Pons)

Formalizations in Coq

• A small compiler for an imperative language, and the proof of its correctness,
• A tiny bytecode verifier for object initialization in Java bytecode.