An Improved Implementation and Abstract Interface for Hybrid

Alan J. Martin
(University of Ottawa)
Amy P. Felty
(University of Ottawa)

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.

In Herman Geuvers and Gopalan Nadathur: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), Nijmegen, The Netherlands, August 26, 2011, Electronic Proceedings in Theoretical Computer Science 71, pp. 76–90.
Published: 31st October 2011.

ArXived at: https://dx.doi.org/10.4204/EPTCS.71.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org