OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.ub.uni-frankfurt.de/index/index/
Thu, 07 Aug 2014 14:56:08 +0200Thu, 07 Aug 2014 14:56:08 +0200Towards correctness of program transformations through unification and critical pair computation
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34439
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, and then of so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems.We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study we apply the method to a lambda calculus with recursive let-expressions and describe an effective unification algorithm to determine all overlaps of a set of transformations with all reduction rules. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modelling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions.Conrad Rau; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34439Tue, 08 Jul 2014 14:56:08 +0200Encoding induction in correctness proofs of program transformations as a termination problem
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/26997
The diagram-based method to prove correctness of program transformations consists of computing
complete set of (forking and commuting) diagrams, acting on sequences of standard reductions
and program transformations. In many cases, the only missing step for proving correctness of a
program transformation is to show the termination of the rearrangement of the sequences. Therefore
we encode complete sets of diagrams as term rewriting systems and use an automated tool
to show termination, which provides a further step in the automation of the inductive step in
correctness proofs.Conrad Rau; David Sabel; Manfred Schmidt-Schaußconferenceobjecthttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/26997Mon, 29 Oct 2012 16:09:25 +0100Computing overlappings by unification in the deterministic lambda calculus LR with letrec, case, constructors, seq and variable chains
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22714
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules.The method is similar to the computation of critical pairs for the completion of term rewriting systems. We describe an effective unification algorithm to determine all overlaps of transformations with reduction rules for the lambda calculus LR which comprises a recursive let-expressions, constructor applications, case expressions and a seq construct for strict evaluation. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modeling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions. As a result the algorithm computes a finite set of overlappings for the reduction rules of the calculus LR that serve as a starting point to the automatization of the analysis of program transformations.Conrad Rau; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22714Thu, 15 Sep 2011 14:20:40 +0200Towards correctness of program transformations through unification and critical pair computation
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7940
Conrad Rau; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7940Sat, 04 Sep 2010 13:04:42 +0200