TY  - UNPD
A1  - Sabel, David
T1  - Alpha-renaming of higher-order meta-expressions
T2  - Frankfurter Informatik-Berichte [; Nr. 2007,2]
N2  - Motivated by tools for automaed deduction on functional programming languages and programs, we propose a formalism to symbolically represent $\alpha$-renamings for meta-expressions. The formalism is an extension of usual higher-order meta-syntax which allows to $\alpha$-rename all valid ground instances of a meta-expression to fulfill the distinct variable convention. The renaming mechanism  may be helpful for several reasoning tasks in deduction systems. We present our approach for a meta-language which uses higher-order abstract syntax and a meta-notation for recursive let-bindings, contexts, and environments. It is used in the LRSX Tool -- a tool to reason on the correctness of program transformations in higher-order program calculi with respect to their operational semantics. Besides introducing a formalism to represent symbolic $\alpha$-renamings, we present and analyze algorithms for simplification of $\alpha$-renamings, matching, rewriting, and checking $\alpha$-equivalence of symbolically $\alpha$-renamed meta-expressions.
T3  - Frankfurter Informatik-Berichte - [2017, 2] 
KW  - Programmiersprachen
KW  - Semantik
KW  - Umbenennung
KW  - Alpha equivalence
KW  - alpha renaming
KW  - meta languages
Y1  - 2017
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/44315
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-443156
SN  - 1868-8330
PB  - Goethe-Univ., Fachbereich Informatik und Mathematik, Institut für Informatik
CY  - Frankfurt am Main
ER  -