The following paper has recently been accepted and published by the Annals of Pure and Applied Logic.
Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic,
by Chuck Liang and Dale Miller.
Available online from http://dx.doi.org/10.1016/j.apal.2012.09.005 and
http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pil-final.pdf .
