TY - GEN

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

AU - Gunter, Elsa L.

AU - Osborn, Christopher J.

AU - Popescu, Andrei

PY - 2009/11/27

Y1 - 2009/11/27

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

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

KW - Axiomatic classes

KW - Isabelle/HOL

KW - Proper functions

KW - Syntax with bindings

KW - Weak hoas

UR - http://www.scopus.com/inward/record.url?scp=70450192868&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70450192868&partnerID=8YFLogxK

U2 - 10.1145/1577824.1577827

DO - 10.1145/1577824.1577827

M3 - Conference contribution

AN - SCOPUS:70450192868

SN - 9781605585291

T3 - ACM International Conference Proceeding Series

SP - 12

EP - 20

BT - LFMTP 2009 - Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages

T2 - 4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009

Y2 - 2 August 2009 through 2 August 2009

ER -