activity
20152022
most citedSimulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq

7 citations · 16 across the 10 of their papers we have counts for

collaborators

10 papers

cs.LO2022★ 1 cited

A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version

David Sabel, Manfred Schmidt-Schauß, Luca Maio

To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arg…

cs.LO2021

Minimal Translations from Synchronous Communication to Synchronizing Locks

Manfred Schmidt-Schauß, David Sabel

In order to understand the relative expressive power of larger concurrent programming languages, we analyze translations of small process calculi which model the communication and…

cs.LO2021

Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version)

Manfred Schmidt-Schauß, David Sabel

In order to understand the relative expressive power of larger concurrent programming languages, we analyze translations of small process calculi which model the communication and…

cs.LO2021

Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Extended Version)

Michael Christian Fink Amores, David Sabel

Motivated by questions from program transformations, eight notions of isomorphisms between term rewriting systems are defined, analysed, and classified. The notions include global…

cs.PL2020★ 1 cited

Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars

Manfred Schmidt-Schauß, David Sabel

Comparison of concurrent programming languages and correctness of program transformations in concurrency are the focus of this research. As criterion we use contextual semantics ad…

cs.LO2019★ 1 cited

Automating the Diagram Method to Prove Correctness of Program Transformations

David Sabel

We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur…