TY  - UNPD
A1  - Schwinghammer, Jan
A1  - Sabel, David
A1  - Niehren, Joachim
A1  - Schmidt-Schauß, Manfred
T1  - On correctness of buffer implementations in a concurrent lambda calculus with futures
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 37
N2  - Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 37 [v.2] 
KW  - Funktionale Programmiersprache
KW  - Lambda-Kalkül
KW  - Nebenläufigkeit
KW  - Pufferspeicher
Y1  - 2009
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34435
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344351
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-37_v2.pdf
IS  - Version: 12 Mai 2005
EP  - 48
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -