5 citations · 6 across the 7 of their papers we have counts for
5 papers · 1 filter
Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
Enguerrand Prebet, André Platzer
Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to…
Uniform Substitution for Differential Refinement Logic
Enguerrand Prebet, André Platzer
This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneousl…
Using Pi-Calculus Names as Locks
Daniel Hirschkoff, Enguerrand Prebet
Locks are a classic data structure for concurrent programming. We introduce a type system to ensure that names of the asynchronous pi-calculus are used as locks. Our calculus also…
On Up-to Context Techniques in the -calculus
Enguerrand Prebet
We present a variant of the theory of compatible functions on relations, due to Sangiorgi and Pous. We show that the up-to context proof technique for bisimulation is compatible in…
On sequentiality and well-bracketing in the -calculus
Daniel Hirschkoff, Enguerrand Prebet, Davide Sangiorgi
The -calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable be…