Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik
4 search hits
- 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.
- 47
-
On conservativity of concurrent Haskell
(2011)
-
David Sabel
Manfred Schmidt-Schauß
- The calculus CHF models Concurrent Haskell extended by
concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional
lambda-calculus which comprises data constructors, case-expressions,
letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent
Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity
of CHF, that is, all equivalences of pure functional expressions are
also valid in CHF. This implies that compiler optimizations and transformations
from pure Haskell remain valid in Concurrent Haskell even if
it is extended by futures. We also show that this is no longer valid if Concurrent
Haskell is extended by the arbitrary use of unsafeInterleaveIO.
- 38
-
Counterexamples to simulation in non-deterministic call-by-need lambda-calculi with letrec
(2009)
-
Manfred Schmidt-Schauß
Elena Machkasova
David Sabel
- 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.
- 35
-
Closures of may and must convergence for contextual equivalence
(2008)
-
Manfred Schmidt-Schauß
David Sabel
- We show on an abstract level that contextual equivalence in non-deterministic program calculi defined by may- and must-convergence is maximal in the following sense. Using also all the test predicates generated by the Boolean, forall- and existential closure of may- and must-convergence does not change the contextual equivalence. The situation is different if may- and total must-convergence is used, where an expression totally must-converges if all reductions are finite and terminate with a value: There is an infinite sequence of test-predicates generated by the Boolean, forall- and existential closure of may- and total must-convergence, which also leads to an infinite sequence of different contextual equalities.
