TY  - THES
A1  - Willig, Martina
T1  - Program equivalences for concurrency abstractions in a concurrent lambda calculus with buffers, cells and futures
N2  - Various concurrency primitives had been added to functional programming languages in different ways. In Haskell such a primitive is a MVar, joins are described in JoCaml and AliceML uses futures to provide a concurrent behaviour. Despite these concurrency libraries seem to behave well, their equivalence between each other has not been proven yet. An expressive formal system is needed. In their paper "On proving the equivalence of concurrency primitives", Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß define a universal calculus for concurrency primitives known as the typed lambda calculus with futures. There, equivalence of processes had been proved. An encoding of simple one-place buffers had been worked out. This bachelor’s thesis is about encoding more complex concurrency abstractions in the lambda calculus with futures and proving correctness of its operational semantics. Given the new abstractions, we will discuss program equivalence between them. Finally, we present a library written in Haskell that exposes futures and our concurrency abstractions as a proof of concept.
KW  - Nebenläufigkeit
KW  - Lambda-Kalkül
KW  - Haskell 98
KW  - concurrency
KW  - lambda calculus
KW  - futures
KW  - programming languages design
KW  - haskell
Y1  - 2009
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7210
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-67958
ER  -