Room 206 (2nd floor, badged access)
16 octobre 2025 - 14h00
Representing and reasoning about nondeterministic programs
par Nicolas Chappe de Verimag
invité(e) par David MONNIAUX
16 octobre 2025 - 14h00
Representing and reasoning about nondeterministic programs
par Nicolas Chappe de Verimag
invité(e) par David MONNIAUX
Abstract: Nondeterminism plays a key role in various aspects of the semantics of programming languages: concurrency, undefined behaviors, weak memory models, etc.
However, the formalization of nondeterministic semantics can be subtle.
I will talk about several contributions I have made over the past few years to help reasoning about such nondeterministic programs.
First, I am a major contributor to the Choice Trees Rocq library, which aims to be to nondeterministic programs what the Interaction Trees library is to deterministic programs: a set of tools to define and reason about executable semantics. This is achieved in particular through the use of modern coinduction up-to companion.
Building on this work, we proposed a layered model of concurrency based on Choice Trees, demonstrating the fitness of Choice Trees for the encoding of the semantics of concurrent programming languages. This model is instantiated in Rocq on a small concurrent subset of LLVM IR with a weak concurrent memory model.
Finally, I recently developed a library of 12 refinements for programs represented as nondeterministic LTSs. Some of these refinements critically rely on a novel mutually coinductive characterization of divergence preservation. I demonstrate the applicabilty of this library by adapting the proof of correctness of a CompCert pass, and by defining a parameterized equational theory of refinement for Choice Trees.
Candidat potentiel à un poste CR CNRS.
