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

• Main Author: Battell, Chelsea
• Other Authors: Felty, Amy
• Language: en
• Published: Université d'Ottawa / University of Ottawa 2016
• Subjects: cut admissibility; structural rules; interactive theorem proving; inductive reasoning; Coq; logical frameworks; higher-order abstract syntax
• Online Access: http://hdl.handle.net/10393/35264; http://dx.doi.org/10.20381/ruor-222

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.