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

On conservativity of concurrent Haskell
(2011)

David Sabel
Manfred SchmidtSchauß
 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
lambdacalculus which comprises data constructors, caseexpressions,
letrecexpressions, 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 nondeterministic callbyneed lambdacalculi with letrec
(2009)

Manfred SchmidtSchauß
Elena Machkasova
David Sabel
 This note shows that in nondeterministic 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 SchmidtSchauß
David Sabel
 We show on an abstract level that contextual equivalence in nondeterministic program calculi defined by may and mustconvergence is maximal in the following sense. Using also all the test predicates generated by the Boolean, forall and existential closure of may and mustconvergence does not change the contextual equivalence. The situation is different if may and total mustconvergence is used, where an expression totally mustconverges if all reductions are finite and terminate with a value: There is an infinite sequence of testpredicates generated by the Boolean, forall and existential closure of may and total mustconvergence, which also leads to an infinite sequence of different contextual equalities.