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

Description
Title: The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
Authors: Battell, Chelsea
Date: 2016
Abstract: 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.
URL: http://hdl.handle.net/10393/35264
http://dx.doi.org/10.20381/ruor-222
CollectionThèses, 2011 - // Theses, 2011 -
Files