TY  - UNPD
A1  - Sabel, David
T1  - Rewriting of higher-order-meta-expressions with recursive bindings
T2  - Frankfurter Informatik-Berichte [; Nr. 2007,1]
N2  - We introduce rewriting of meta-expressions which stem from a meta-language that uses higher-order abstract syntax augmented by meta-notation for recursive let, contexts, sets of bindings, and chain variables. Additionally, three kinds of constraints can be added to meta-expressions to express usual constraints on evaluation rules and program transformations. Rewriting of meta-expressions is required for automated reasoning on programs and their properties. A concrete application is a procedure to automatically prove correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. Rewriting on meta-expressions can be performed by solving the so-called letrec matching problem which we introduce. We provide a matching algorithm to solve it. We show that the letrec matching problem is NP-complete, that our matching algorithm is sound and complete, and that it runs in non-deterministic polynomial time.
T3  - Frankfurter Informatik-Berichte - [2017, 1] 
KW  - Terrmersetzungssystem
KW  - Reduktionssystem
KW  - matching
KW  - rewriting
KW  - verification
KW  - program transformation
Y1  - 2017
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/44314
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-443148
SN  - 1868-8330
PB  - Goethe-Univ., Fachbereich Informatik und Mathematik, Institut für Informatik
CY  - Frankfurt am Main
ER  -