Theory support for weak higher order abstract syntax in isabelle/HOL

Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We describe the theoretical underpinnings to support the construction of an extension to the Isabelle/HOL theorem prover to support the creation of datatypes for weak higher-order abstract syntax, and give an example of its application. This theoretical basis is centered around the concept of variable types (i.e. types whose elements are variables), and the concept of two terms in a given type having the "same structure" up to a given set of substitutions (the difference set) of one variable for another as allowed by that set. We provide an axiomatization of types for which the notion of having the same structure is well-behaved with the axiomatic class of same struct thy. We show that being a same struct thy is preserved by products, sums and certain function spaces. Within a same struct thy, not all terms necessarily have the same structure as anything, including themselves. Those terms having the same structure as themselves relative to the empty difference set are said to be proper. A proper function from variables to terms corresponds to an abstraction of a variable in a term and also corresponds to substitution of variables for that variable in the term. Proper functions form the basis for a formalization of weak higherorder abstract syntax.

Original languageEnglish (US)
Title of host publicationLFMTP 2009 - Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages
Subtitle of host publicationTheory and Practice
Number of pages9
StatePublished - 2009
Event4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 - Montreal, QC, Canada
Duration: Aug 2 2009Aug 2 2009

Publication series

NameACM International Conference Proceeding Series


Other4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009
CityMontreal, QC


  • Axiomatic classes
  • Isabelle/HOL
  • Proper functions
  • Syntax with bindings
  • Weak hoas

ASJC Scopus subject areas

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications


Dive into the research topics of 'Theory support for weak higher order abstract syntax in isabelle/HOL'. Together they form a unique fingerprint.

Cite this