OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.stub.uni-frankfurt.de/index/index/
Thu, 03 Jul 2008 16:07:51 +0100Thu, 03 Jul 2008 16:07:51 +0100Adequacy of compositional translations for observational semantics
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/192
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and must-convergence in arbitrary contexts, and adequacy of translations, i.e., the reﬂection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extension.Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/192Fri, 07 Mar 2008 16:07:51 +0100A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/191
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus' semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as non-determinism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe's proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.Manfred Schmidt-Schauß; Elena Machkasovaworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/191Fri, 07 Mar 2008 16:05:42 +0100Program Equivalence for a Concurrent Lambda Calculus with Futures
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/2181
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.Joachim Niehren; David Sabel; Manfred Schmidt-Schauß; Jan Schwinghammerworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/2181Mon, 30 Oct 2006 08:54:30 +0100