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

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...

Full description

Bibliographic Details
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

Internet

http://hdl.handle.net/10393/35264
http://dx.doi.org/10.20381/ruor-222

Similar Items