Chelsea Battell

The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid

2016

Hybrid is a logical framework that supports the use of higher-order abstract syntax (HOAS) in representing formal systems or "object logics" (OLs). It is implemented in Coq and follows a two-level approach, where a specification …