Interactive proof assistants are great at reasoning inside the meta-logic for which they were designed. Even general purpose proof assistant, such as Isabelle, more or less requires that users pick a specific Isabelle instance (typically Isabelle/HOL) to work effectively. When working with program logics this becomes problematic since we by necessity create our own logics to reason about our programs. To name a few we use separation logic to reason about programs with mutable state, Hoare logic to reason about the specifications of programs, and we have different instances of these logics where some reason about the stack or the heap, and where some don't, and so on. Defining these logics in a proof assistant is not difficult. Reasoning in these logics, however, is challenging, tedious, and cumbersome.
Charge! is a logical framework for Coq designed to allow users to define their own logics inside Coq and use them effectively for proofs using built in tactics and heuristics. We accomplish this by using Coq's built in support for type classes. Using these, we can tell Coq what it means to be an intuitionistic logic (like the meta-logic that Coq currently supports), what it means to be a separation logic, what it means to be a modal logic, and so on. On top of these definitions we can then create tactics that will work for all possible instances of these type classes - not just the ones that the developers originally envisioned.
We are currently working on the next stable release of the language independent version of Charge!, and it will be made available on github by the end of August 2013.