Refine
Year of publication
Document Type
- Working Paper (10)
- Article (8)
- Conference Proceeding (3)
Has Fulltext
- yes (21)
Is part of the Bibliography
- no (21)
Keywords
- Lambda-Kalkül (8)
- Operationale Semantik (6)
- Programmiersprache (5)
- Nebenläufigkeit (3)
- Funktionale Programmiersprache (2)
- Pufferspeicher (2)
- Alice ML (1)
- Contextual Equivalence (1)
- Futures (1)
- Glioblastoma (1)
Institute
- Informatik (10)
- Neuere Philologien (10)
- Medizin (1)
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.
Motivated by our experience in analyzing properties of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods, constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness. The presented framework can directly be applied to the observational equivalences derived from the operational semantics of programming calculi, and also to other situations, and thus has a wide range of applications.
Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
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.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and must-convergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extension.
Purpose: The role of obesity in glioblastoma remains unclear, as previous analyses have reported contradicting results. Here, we evaluate the prognostic impact of obesity in two trial populations; CeTeG/NOA-09 (n = 129) for MGMT methylated glioblastoma patients comparing temozolomide (TMZ) to lomustine/TMZ, and GLARIUS (n = 170) for MGMT unmethylated glioblastoma patients comparing TMZ to bevacizumab/irinotecan, both in addition to surgery and radiotherapy.
Methods: The impact of obesity (BMI ≥ 30 kg/m2) on overall survival (OS) and progression-free survival (PFS) was investigated with Kaplan–Meier analysis and log-rank tests. A multivariable Cox regression analysis was performed including known prognostic factors as covariables.
Results: Overall, 22.6% of patients (67 of 297) were obese. Obesity was associated with shorter survival in patients with MGMT methylated glioblastoma (median OS 22.9 (95% CI 17.7–30.8) vs. 43.2 (32.5–54.4) months for obese and non-obese patients respectively, p = 0.001), but not in MGMT unmethylated glioblastoma (median OS 17.1 (15.8–18.9) vs 17.6 (14.7–20.8) months, p = 0.26). The prognostic impact of obesity in MGMT methylated glioblastoma was confirmed in a multivariable Cox regression (adjusted odds ratio: 2.57 (95% CI 1.53–4.31), p < 0.001) adjusted for age, sex, extent of resection, baseline steroids, Karnofsky performance score, and treatment arm.
Conclusion: Obesity was associated with shorter survival in MGMT methylated, but not in MGMT unmethylated glioblastoma patients.