Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik
3 search hits
- 50
-
Correctness of an STM Haskell implementation
(2012)
-
Manfred Schmidt-Schauß
David Sabel
- A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of con
icting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence.
This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
- 49
-
Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq
(2012)
-
Manfred Schmidt-Schauß
David Sabel
Elena Machkasova
- This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual
approximation into a call-by-name calculus, which is an extension
of Abramsky's lazy lambda calculus. In the latter calculus equivalence
of similarity and contextual approximation can be shown by Howe's
method. Using an equivalent but inductive definition of behavioral preorder
we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
- 48
-
An abstract machine for concurrent Haskell with futures
(2012)
-
David Sabel
- We show how Sestoft’s abstract machine for lazy evaluation
of purely functional programs can be extended to evaluate expressions of
the calculus CHF – a process calculus that models Concurrent Haskell
extended by imperative and implicit futures. The abstract machine is
modularly constructed by first adding monadic IO-actions to the machine
and then in a second step we add concurrency. Our main result is that
the abstract machine coincides with the original operational semantics
of CHF, w.r.t. may- and should-convergence.
