Informatik
Refine
Year of publication
- 2009 (21) (remove)
Document Type
- Working Paper (9)
- Article (5)
- Doctoral Thesis (3)
- Conference Proceeding (2)
- Bachelor Thesis (1)
- Book (1)
Language
- English (21) (remove)
Has Fulltext
- yes (21)
Is part of the Bibliography
- no (21)
Keywords
- Lambda-Kalkül (6)
- Nebenläufigkeit (3)
- Funktionale Programmiersprache (2)
- Operationale Semantik (2)
- Programmiersprache (2)
- Pufferspeicher (2)
- Algorithmus (1)
- Flash Memories (1)
- Formale Semantik (1)
- Haskell 98 (1)
- Kontextuelle Gleichheit (1)
- Nichtdeterminismus (1)
- Online Algorithms (1)
- Paging Algorithms (1)
- Rènyi mutual information (1)
- Seitenersetzungsstrategie (1)
- Takens-Grassberger correlation integral (1)
- ambiguity (1)
- automata (1)
- classification (1)
- clustering (1)
- communication complexity (1)
- concurrency (1)
- contextual equivalence (1)
- data streams (1)
- feature selection (1)
- futures (1)
- haskell (1)
- lambda calculus (1)
- lower bounds (1)
- machine models (1)
- non-determinism (1)
- nondeterministic finite automata (1)
- process approximation (1)
- programming languages design (1)
- semantics (1)
- the set disjointness problem (1)
Institute
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. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide 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.