DyVerSe

Dynamic Versatile Semantics

Contact

Pierre Clairambault, pierre.clairambault@ens-lyon.fr

People

  • Permanent members:
    • LIP, ENS Lyon:
      • Pierre Clairambault (coordinator), CNRS
      • Olivier Laurent, CNRS
      • Colin Riba, MCF
    • LS2N, Nantes:
      • Guillaume Munch-Maccagnoni, Inria
    • IRISA, Rennes:
      • Simon Castellan, CR Inria, Rennes.
  • Non-permanent members:
    • Lison Blondeau-Patissier, ENS Lyon.
  • Collaborators:
    • Aurore Alcolei, Postdoc, Bologna, Italy.
    • Marc de Visme, Postdoc, LORIA, Nancy.
    • Hugo Paquet, Postdoc, Oxford, UK.
    • Glynn Winskel, Professor, Cambridge, UK.

Presentation

DyVerSe aims to develop a theoretical framework for dynamic/game semantics for programming languages, capturing in one versatile setting a spectrum of computational features, representative of the heterogeneity of software (e.g. higher-order functions, concurrency, probabilities or other quantitative aspects). Our ambition is (1) to help unify denotational semantics by providing the missing link between various incompatible models focusing on specific aspects, and (2) to provide a toolbox to reason compositionally about the dynamic behaviour of programs, with an eye towards specification and verification.

The scientific proposal can be found here.

News

  • 06/11/2020: First Concurrent Games Café.
  • 28/09/2020: Marc de Visme successully defended his PhD thesis.
  • 01/01/2020: DyVerSe starts!

Publications

  • Lison Blondeau-Patissier and Pierre Clairambault. Positional Injectivity for Innocent Strategies.
    Accepted in FSCD 2021. [pdf]

  • Pierre Clairambault and Marc de Visme. Full Abstraction for the Quantum Lambda-Calculus.
    POPL 2020. [pdf]

Software

  • Causal Ocaml, and implementation of the concurrent game semantics of a fragment of Ocaml by Simon Castellan

Animation

The Concurrent Games Café is a series of virtual talks around the topics of DyVerSe. See more information here.