The Logic of Hereditary Harrop Formulas as a Specification
Logic for Hybrid,
by Chelsea Battell and Amy Felty.
In Proceedings of the Eleventh International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP),
The files run in Coq V8.5.
The first must be compiled before loading the second.