DyVerSe

Dynamic Versatile Semantics

Contact

Pierre Clairambault, pierre.clairambault@cnrs.fr

People

  • Permanent members:
    • LIP, ENS Lyon:
      • Olivier Laurent, CNRS
      • Colin Riba, MCF
    • LIS, Aix-Marseille Université
      • Pierre Clairambault, CNRS
    • LS2N, Nantes:
      • Guillaume Munch-Maccagnoni, Inria
    • IRISA, Rennes:
      • Simon Castellan, CR Inria, Rennes.

  • Non-permanent members:
    • Lison Blondeau-Patissier, Aix-Marseille Université.
    • Simon Forest, Aix-Marseille Université, postdoc DyVerSe.

  • Collaborators:
    • Aurore Alcolei, Postdoc, LACL, UPEC.
    • Marc de Visme, Inria, LMF, Université Paris-Saclay.
    • Hugo Paquet, Postdoc MSCA, LIPN, Université Paris 13.
    • Glynn Winskel, HUAWEI, Edimbourg.

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.












Publications

  • Pierre Clairambault and Simon Forest. The Cartesian Closed Category of Thin Spans of Groupoids.
    Accepted in LICS 2023. [arXiv]

  • Pierre Clairambault, Federico Olimpieri and Hugo Paquet. From Thin Concurrent Games to Generalized Species of Structures.
    Accepted in LICS 2023. [arXiv]

  • Pierre Clairambault, Lison Blondeau-Patissier and Lionel Vaux-Auclair. Strategies as Resource Terms, and their Categorical Semantics.
    Accepted in FSCD 2023. [arXiv]

  • Simon Castellan and Pierre Clairambault. The Geometry of Causality : Multi-Token Geometry of Interaction and its Causal Unfolding.
    In POPL 2023. [HAL]

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

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

Software

  • IPA to Petri Nets, the accompanying implementation to this paper, evaluated by the artifact evaluation committee for POPL 2023.

  • 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.