An Improved Implementation and Abstract Interface for Hybrid

TL;DR

This paper enhances the Hybrid framework in Isabelle/HOL by developing an abstract, mathematically rigorous interface that simplifies reasoning about object languages using higher-order abstract syntax, with practical benefits for proofs.

Contribution

The paper introduces an improved, more abstract interface for Hybrid that better encapsulates de Bruijn indices and facilitates higher-level reasoning about object languages.

Findings

New proof of adequacy for Hybrid

Enhanced reasoning capabilities for object logics

Complete characterization of Hybrid primitives at HOAS level

Abstract

Hybrid is a formal theory implemented in Isabelle/HOL that provides an interface for representing and reasoning about object languages using higher-order abstract syntax (HOAS). This interface is built around an HOAS variable-binding operator that is constructed definitionally from a de Bruijn index representation. In this paper we make a variety of improvements to Hybrid, culminating in an abstract interface that on one hand makes Hybrid a more mathematically satisfactory theory, and on the other hand has important practical benefits. We start with a modification of Hybrid's type of terms that better hides its implementation in terms of de Bruijn indices, by excluding at the type level terms with dangling indices. We present an improved set of definitions, and a series of new lemmas that provide a complete characterization of Hybrid's primitives in terms of properties stated at the HOAS level. Benefits of this new package include a new proof of adequacy and improvements to reasoning about object logics. Such proofs are carried out at the higher level with no involvement of the lower level de Bruijn syntax.