Logo des Repositoriums

Auflistung nach Autor:in "Sabel, David"

1 - 4 von 4
  • Konferenzbeitrag
    An abstract machine for concurrent haskell with futures
    (Software Engineering 2012. Workshopband, 2012) Sabel, David
    We show how Sestoft's abstract machine for lazy evaluation of purely functional programs can be extended to evaluate expressions of the calculus CHF – a process calculus that models Concurrent Haskell extended by imperative and implicit futures. The abstract machine is modularly constructed by first adding monadic IO-actions to the machine and then in a second step we add concurrency. Our main result is that the abstract machine coincides with the original operational semantics of CHF, w.r.t. mayand should-convergence.
  • Konferenzbeitrag
    Parallelizing DPLL in Haskell
    (Software Engineering 2013 - Workshopband, 2013) Berger, Till; Sabel, David
    We report on a case study of implementing parallel variants of the Davis- Putnam-Logemann-Loveland algorithm for solving the SAT problem of propositional formulas in the functional programming language Haskell. We explore several state of the art programming techniques for parallel and concurrent programming in Haskell and provide the corresponding implementations. Based on our experimental results, we compare several approaches and implementations.
  • Konferenzbeitrag
    Reasoning about contextual equivalence: From untyped to polymorphically typed Calculi
    (Informatik 2009 – Im Focus das Leben, 2009) Sabel, David; Schmidt-Schauß, Manfred; Harwath, Frederik
  • Textdokument
    Semantik eines verzögert auswertenden Lambdakalküls mit McCarthy’s amb für Programmäquivalenz
    (Ausgezeichnete Informatikdissertationen 2008, 2009) Sabel, David
    In diesem Beitrag werden die Ergebnisse der Untersuchung eines verzögert-auswertenden Lambdakalküls höherer Ordnung mit case-Ausdrücken, rekursivem let-rec, einem seq-Operator und einem nichtdeterministischen Divergenz-vermeidenden Operatoramb dargestellt. Als Gleichheitsbegriff wird kontextuelle Äquivalenzbzgl. einer May- und Must-Konvergenz verwendet. Mithilfe syntaktischer Methoden wird die Korrektheit von Programmtransformationen nachgewiesen und die Korrektheit von Übersetzungenuntersucht.U.a.werden ein Kontextlemma, ein Standardisierungstheorem und die Gültigkeit einer endlichen Simulation gezeigt.