OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.ub.uni-frankfurt.de/index/index/
Thu, 07 Aug 2014 14:12:40 +0200Thu, 07 Aug 2014 14:12:40 +0200On correctness of buffer implementations in a concurrent lambda calculus with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34435
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34435Tue, 08 Jul 2014 14:12:40 +0200Adequacy of compositional translations for observational semantics
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34433
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection 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 extensions.Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34433Tue, 08 Jul 2014 14:02:58 +0200A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34429
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 nondeterminism, 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.ub.uni-frankfurt.de/frontdoor/index/index/docId/34429Tue, 08 Jul 2014 13:30:21 +0200On equivalences and standardization in a non-deterministic call-by-need lambda calculus
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34451
The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in an extended lambda-calculus LS with case, constructors, seq, let, and choice, with a simple set of reduction rules; and to argue that an approximation calculus LA is equivalent to LS w.r.t. the contextual preorder, which enables the proof tool of simulation. Unfortunately, a direct proof appears to be impossible.
The correctness proof is by defining another calculus L comprising the complex variants of copy, case-reduction and seq-reductions that use variable-binding chains. This complex calculus has well-behaved diagrams and allows a proof of correctness of transformations, and that the simple calculus LS, the calculus L, and the calculus LA all have an equivalent contextual preorder.Manfred Schmidt-Schauß; Matthias Mannworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34451Tue, 08 Jul 2014 12:16:49 +0200Counterexamples to simulation in non-deterministic call-by-need lambda-calculi with letrec
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7827
This note shows that in non-deterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors.Manfred Schmidt-Schauß; Elena Machkasova; David Sabelworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7827Tue, 22 Jun 2010 17:45:50 +0200Contextual equivalence in lambda-calculi extended with letrec and with a parametric polymorphic type system
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6667
This paper describes a method to treat contextual equivalence in polymorphically typed lambda-calculi, and also how to transfer equivalences from the untyped versions of lambda-calculi to their typed variant, where our specific calculus has letrec, recursive types and is nondeterministic. An addition of a type label to every subexpression is all that is needed, together with some natural constraints for the consistency of the type labels and well-scopedness of expressions. One result is that an elementary but typed notion of program transformation is obtained and that untyped contextual equivalences also hold in the typed calculus as long as the expressions are well-typed. In order to have a nice interaction between reduction and typing, some reduction rules have to be accompanied with a type modification by generalizing or instantiating types.Manfred Schmidt-Schauß; David Sabel; Frederik Harwathworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6667Tue, 07 Jul 2009 13:30:55 +0200On correctness of buffer implementations in a concurrent lambda calculus with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666Tue, 07 Jul 2009 13:22:26 +0200