Séminaires

Over the last few years, we have been experimenting with using flavours of (coinductive) monadic interpreters to represent computations in Rocq. The basic toolbox of the approach has been embedded back in 2020 in the Interaction Trees library, and notably used at scale in the Vellvm project to give a formal semantics to LLVM IR. In this talk, I will walk through this experience, with the aim to focus in particular on the comparatively more recent treatment of non-determinism. I will introduce so-called Choice Trees, a second library adding support for a choice operator. On top of this primitive operation, we implement shallow combinators for various flavours of parallel composition, whether w.r.t. to shared memory model or communication-based computations. Furthermore, additionally to the monadic interpretation of operations, choice trees support refinements of its internal branching, allowing for executing the semantics against specific schedulers, whether internally to Rocq or on the OCaml side. Finally, and if time permit, I will move the focus to ongoing work with Peio Borthelle around, for lack of talent in naming, monadic trees. This time, we step back to a mathematically more natural approach, albeit more challenging to implement: rather than implementing effect through monad transformers on top of itrees, we directly construct the final coalgebra of the composition of a monad `m` with a functor of observation. ITrees become the specialised case where "m=id", CTrees are essentially isomorphic to the case of "m=fam", the functor of families, and a more generic theory can be established.

La bisimulation est une technique de preuve pour montrer que 2 programmes "font la même chose". Je ferai un panorama rapide des bisimulations pour le lambda-calcul, avant de faire l'état de l'art des bisimulations définies jusqu'ici pour les calculs "linéaires" et voir quelles questions restent pour l'instant non résolues.

While the ?-calculus is widely recognized as a model of computation, equivalent to Turing and other machines, its relevance for the study of complexity has long been unclear. Its central operation, ?-reduction, seems at first sight too rich and complex to be considered as an appropriate atomic unit of computation. We learned only quite recently that the natural complexity measures (number of ?-reductions for time, size of terms for space) were indeed ''reasonable'' measures, defining the same complexity classes (P, NP, PSPACE, ...) as the Turing standard. In this talk I will propose a refined —but still simple and natural— definition of space complexity for the ?-calculus, sensitive to sub-linear space. In particular, this measure allows a ?-calculus-based characterization of algorithms running in logarithmic space (class L), thus extending the range of complexity classes for which the ?-calculus is an appropriate vessel.

As originally showed by Barr, a topology on a set X can be equivalently described as a 'convergence relation' between elements of X and ultrafilters on X: in other words, a spatial locale can be recovered from its set of points once it is endowed with appropriate extra structure defined in terms of ultrafilters. In this talk, I will present a similar reconstruction result for (Grothendieck) toposes with enough points, a categorification of spatial locales: every such topos can be recovered up to equivalence from its category of points, provided that the latter is endowed with appropriate extra structure involving ultrafilters. In logical terms, this reads as a (strong) conceptual completeness theorem for geometric logic. Towards this goal, I will introduce ultraconvergence spaces, a profunctorial generalization of Makkai's ultracategories inspired by Barr's convergence relations. This talk is based on joint work with Quentin Aristote, Sam van Gool and Jérémie Marquès.

A fundamental operation in type systems is the ability to *type cast*, that is, take a value of a given type and use it at different type, assuming some information relating the source and target. This manifests under many names: subtyping, coercion, transport... These various mechanisms are particularly essential in dependent type theory, where types are extremely rich and precise. Yet they have a complicated history, and are rather poorly understood from a theoretical standpoint. In my talk I will explain the challenges faced with cast systems, and how we can understand and fix some of them with the type theorist's glasses on. The focus will be particularly on *structural* casts, those that follow the structure of type formers, which led us to a surprisingly deep and beautiful type theoretic quest, revolving around the idea that structural casts arise from the fact that all type formers are really functors.

Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abstraction functions to demonstrate the coherence between such concrete implementations and their abstract specifications. However, the Hoare methodology relies on a conventional separation between implementation and specification, providing no linguistic support for ensuring that this convention is obeyed. The presented work proposes a synthetic account of Hoare's methodology within univalent dependent type theory by encoding the data of abstraction functions within types themselves. This is achieved via a phase distinction, which gives rise to a gluing construction that renders an abstraction function as a type and a pair of modalities that fracture a type into its concrete and abstract parts. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory. This approach scales to verification of cost, allowing the analysis of client cost relative to a cost-aware specification. A monadic sealing effect facilitates modularity of cost, permitting an implementation to be upper-bounded by its specification in cases where private details influence observable cost. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.