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 admissibility; results that greatly simplify reasoning about OLs in systems providing HOAS. The SL is a sequent calculus defined as an inductive type in Coq and we prove properties by structural induction over SL sequents. We also present a generalized SL and metatheory statement, allowing us to prove many cases of such theorems in a general way and understand how to identify and prove the difficult cases. We make a concrete and measurable improvement to Hybrid with the new SL formalization and provide a technique for abstracting such proofs, leading to a condensed presentation, greater understanding, and a generalization that may be instantiated to other logics.
| Identifer | oai:union.ndltd.org:uottawa.ca/oai:ruor.uottawa.ca:10393/35264 |
| Date | January 2016 |
| Creators | Battell, Chelsea |
| Contributors | Felty, Amy |
| Publisher | Université d'Ottawa / University of Ottawa |
| Source Sets | Université d’Ottawa |
| Language | English |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.0018 seconds