Electronic Appendix

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), June 2016 (pdf).

The files run in Coq V8.5. The first must be compiled before loading the second.