A model of Java in Coq based on the Charge! framework.