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.
 44

A contextual semantics for concurrent Haskell with futures
(2011)

David Sabel
Manfred SchmidtSchauß
 In this paper we analyze the semantics of a higherorder functional language with concurrent threads, monadic IO and synchronizing variables as in Concurrent Haskell. To assure declarativeness of concurrent programming we extend the language by implicit, monadic, and concurrent futures. As semantic model we introduce and analyze the process calculus CHF, which represents a typed core language of Concurrent Haskell extended by concurrent futures. Evaluation in CHF is defined by a smallstep reduction relation. Using contextual equivalence based on may and shouldconvergence as program equivalence, we show that various transformations preserve program equivalence. We establish a context lemma easing those correctness proofs. An important result is that callbyneed and callbyname evaluation are equivalent in CHF, since they induce the same program equivalence. Finally we show that the monad laws hold in CHF under mild restrictions on Haskell’s seqoperator, which for instance justifies the use of the donotation.
 39 [v.4]

Reconstructing a logic for inductive proofs of properties of functional programs
(2011)

David Sabel
Manfred SchmidtSchauß