The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
Hybrid is a two-level logical framework that supports higher-order abstract syntax (HOAS), where a specification logic (SL) extends the class of object logics (OLs) we can reason about. We develop a new Hybrid SL and formalize its metatheory, proving weakening, contraction, exchange, and cut admis...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en |
| Published: |
Université d'Ottawa / University of Ottawa
2016
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10393/35264 http://dx.doi.org/10.20381/ruor-222 |