OPUS 4 | Search

search hits 1551 to 1560

Sort by

Franz Kafka und das Judentum : Einführung in Kafkas Leben und Entwicklung (2009)
Ursula Homann

Hat das Jiddische sein letztes Wort noch nicht gesprochen : jiddische Sprache und jiddische Literatur ohne Basis (2009)
Ursula Homann

Voltaire, Nietzsche und die Juden : waren die Philosophen Hitlers Wegbereiter? (2009)
Ursula Homann

Contextual equivalence in lambda-calculi extended with letrec and with a parametric polymorphic type system (2009)
Manfred Schmidt-Schauß David Sabel Frederik Harwath: This paper describes a method to treat contextual equivalence in polymorphically typed lambda-calculi, and also how to transfer equivalences from the untyped versions of lambda-calculi to their typed variant, where our specific calculus has letrec, recursive types and is nondeterministic. An addition of a type label to every subexpression is all that is needed, together with some natural constraints for the consistency of the type labels and well-scopedness of expressions. One result is that an elementary but typed notion of program transformation is obtained and that untyped contextual equivalences also hold in the typed calculus as long as the expressions are well-typed. In order to have a nice interaction between reduction and typing, some reduction rules have to be accompanied with a type modification by generalizing or instantiating types.

On correctness of buffer implementations in a concurrent lambda calculus with futures (2009)
Jan Schwinghammer David Sabel Joachim Niehren Manfred Schmidt-Schauß: 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.

search hits 1551 to 1560