Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 26

Program Equivalence for a Concurrent Lambda Calculus with Futures
(2006)

Joachim Niehren
David Sabel
Manfred SchmidtSchauß
Jan Schwinghammer
 Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures Lambda(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics.
 24

A callbyneed lambdacalculus with locally bottomavoiding choice : context lemma and correctness of transformations
(2006)

David Sabel
Manfred SchmidtSchauß
 We present a higherorder callbyneed lambda calculus enriched with constructors, caseexpressions, recursive letrecexpressions, a seqoperator for sequential evaluation and a nondeterministic operator amb, which is locally bottomavoiding. We use a smallstep operational semantics in form of a normal order reduction. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into an arbitrary program context their termination behaviour is the same. We use a combination of may as well as mustconvergence, which is appropriate for nondeterministic computations. We evolve different proof tools for proving correctness of program transformations. We provide a context lemma for may as well as must convergence which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with socalled complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations keep contextual equivalence. In contrast to other approaches our syntax as well as semantics does not make use of a heap for sharing expressions. Instead we represent these expressions explicitely via letrecbindings.