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
Y1 - 2009
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 -