English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Correctness of program transformations in extended lambda calculi with acontextual semantics is usually based on reasoning about the operationalsemantics which is a rewrite semantics. A successful approach to provingcorrectness is the combination of a context lemma with the computation ofoverlaps between program transformations and the reduction rules, and then ofso-called complete sets of diagrams. The method is similar to the computationof critical pairs for the completion of term rewriting systems. We explorecases where the computation of these overlaps can be done in a first order wayby variants of critical pair computation that use unification algorithms. As acase study we apply the method to a lambda calculus with recursivelet-expressions and describe an effective unification algorithm to determineall overlaps of a set of transformations with all reduction rules. Theunification algorithm employs many-sorted terms, the equational theory ofleft-commutativity modelling multi-sets, context variables of different kindsand a mechanism for compactly representing binding chains in recursivelet-expressions.

Towards Correctness of Program Transformations Through Unification and Critical Pair Computation