Seminars

I will give you an overview of my recent work on linear logic proof-nets. The common thread is the study of the structural, geometric properties of proofs, and how they are related to the purely logical properties, with particular emphasis on the property of connectivity. I will present some interesting results from two related lines of research on classical and intuitionistic linear logic, and on the connection between proof-nets and the bang calculus. The starting point is a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property states that every correctness graph of the proof-structure is acyclic, and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in MELL (multiplicative exponential linear logic) to recover a sequent calculus proof from a proof-structure. I will present fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting and in the fragment of MELL corresponding to the half-polarized typing system for call-by-push-value by Ehrhard. This fragment of MELL contains the translation of the bang calculus, a generalization of both call-by-name and call-by-value lambda-calculus, and, in particular, the image of the two Girard's translations. I will then explain more in detail the connection between the bang calculus and linear logic proof-nets: cut elimination simulates bang calculus reduction, and Girard's call-by-name and call-by-value translations of the lambda-calculus into proof-nets factor as the composition of the call-by-name and call-by-value translations of the lambda-calculus into the bang calculus with the translation of the bang calculus into proof nets. Finally, I give a geometric characterization of those proof-nets that arise from terms of the bang calculus.

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.

The combination of the theory of differential calculus with the theory of programming languages is an active field of research, with the development of automated differentiation and of the differential lambda calculus. It is well known that differentiation can be turned into a compositional operation, using the tangent bundle construction, also called dual numbers in automated differentiation. In this talk, we explain how Taylor expansion at any degree is also captured by a compositional operation. This operation is similar to jet bundles found in differential geometry, and to higher order dual numbers that have found recent applications in automated differentiation. We will then discuss how category theory is a nice framework to describe those ideas. Formally, Taylor expansion is captured as a functor, and the axioms of differential calculus boil down to naturality equations that turn this functor into a monad. We will then briefly explain how those ideas can be applied to the study Taylor expansion in quantitative semantics of Linear Logic.

OCaml is a multi-paradigm, high-level programming language with years of development and a modern set of features such as concurrency and effect handlers. The Osiris project is an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant. In this talk, I will present OLang, a nontrivial fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers. I will show how we define the dynamic semantics of a realistic language as a monadic interpreter running atop a custom monad where computations are internally represented as trees of operations and effects are interpreted with a small-step semantics. I will present two program logics for OLang: a stateless Hoare Logic allows reasoning about so-called pure programs, and an Iris-based Separation Logic allows reasoning about arbitrary programs.

Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with ?-, ?-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.

Les structures de troncation, ou t-structures, ont été inventées pour remplacer les troncations de Postnikov en homotopie stable. Les modalités ont été inventées en théorie homotopique des types pour axiomatiser les troncations de Postnikov dans les ?-topos. Il se trouve que les deux notions peuvent s’encoder de manière uniforme comme des systèmes de factorisation stables par changement de base. Les examples de modalités abondent : préfaisceaux séparés, morphismes acycliques, A1-localisation, l’élusive modalité de Sullivan... J’expliquerai comment toute modalité vient avec une tour de complétion et comment on peut généraliser la notion de n-topos en t-topos, relatif à une modalité arbitraire.

Differential Linear Logic (DiLL) is a sequent calculus expressing differentiation through symmetries between linear and non-linear formulas. In this talk, we express categorical models of DiLL as a pair of Grothendieck fibrations equipped with a tangent functor. To do so, we adapt methods from categorical semantics of Type Theory to linear-non-linear adjunctions. In the future, we hope this approach will enable the construction of models of a flavor of dependent differential linear logic.

Le séminaire propose une discussion autour de l’opérateur de bar-récursion, son utilisation pour réaliser l’axiome du choix et le lien avec des propriétés très connues au sein de la théorie des algèbres booléennes. On présentera d’abord l’opérateur informellement, en une introduction historique sur sa première définition et sa ressemblance opérationnelle avec le principe de bar-induction. De suite, on abordera la notion de clôture pour une algèbre de Boole, une propriété fondamentale dans le cadre du forcing. On terminera en décrivant la connexion entre l’opérateur et cette propriété dans le cas de la réalisabilité classique, ce qui vient d’un travail avec Laura Fontanella.

Oles embeddings are a way of generalizing the notion of injection in the category of sets (and decidable subobject in an extensive category) to an arbitrary category with finite coproducts. The concept is dual to that of Oles expansions, also known as very well-behaved lenses, which have played a role in the semantics of state. We also introduce notions of Oles inverse image square, Oles intersection square and union, generalizing the corresponding notions from the category of sets and satisfying several of their properties. We then further generalize these notions to the setting of a category acting on another category, and we see various examples from the semantics of effects arising as special cases. These include the lookup/update algebras (mnemoids) of Plotkin and Power, and monads supporting exceptions and other kinds of handling.

La philosophie des sciences éclaire la nature complexe des langages de programmation (dichotomie syntaxe/sémantique (White, 2004) ou fonction/structure (Turner, 2014)). Ces cadres d’analyse sont utiles mais insuffisants pour saisir pleinement leur complexité socio-technique, historiquement évolutive et socialement située. Le langage de programmation Prolog offre un cas d’étude particulièrement intéressant. Contrairement à d’autres langages l’ayant précédé (FORTRAN, COBOL, ALGOL ou encore LISP), Prolog n’est pas conçu de manière descendante à partir de spécifications techniques et d’un champ applicatif, mais émerge de manière itérative à partir d’un outil de démonstration automatique, dans le cadre de recherches menées sur le langage naturel par le Groupe d’Intelligence Artificielle de l’Université de Marseille Luminy au début des années 1970. Cette genèse particulière rend difficile la détermination d’un moment précis d’apparition du langage et nous amène à nous interroger sur les caractéristiques permettant de qualifier un système informatique particulier de langage de programmation. À travers trois tableaux, nous chercherons à montrer que le statut épistémique de Prolog est pluriel et intimement lié au contexte social de production et d’utilisation du langage. En suivant ainsi pas à pas la genèse de Prolog entre Marseille et Edimbourg, nous mettrons en lumière certains aspects méconnus des débuts de la recherche en intelligence artificielle en Europe au début des années 1970, de ses rivalités et de ses controverses.

Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. This talk focuses on an inductive notion of useful call-by-value. Our starting point is the well-known Value Substitution Calculus, refining its substitution operation so that it becomes linear, yielding the LCBV calculus. We then further refine LCBV by restricting linear substitution only when it contributes to the progress of the computation, yielding the UCBV strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Furthermore, the UCBV strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that UCBV can be implemented with polynomial time-overhead by invariant cost models. UCBV is part of the preliminary work required to develop semantic interpretations of useful call-by-value, for which its inductive formulation is more suitable than the (non-inductive) existing ones.

The notion of a local state classifier was introduced in the context of Lawvere's first open problem in topos theory. Although this problem itself has already been resolved, the idea of local state classifiers—defined as colimits of all monomorphisms—has potential applications in more general categorical frameworks beyond topos theory. In this talk, I will not delve into the technical details of topos theory. Instead, I will focus on explaining the definition and core idea of the local state classifier through simple examples. At the end of the presentation, I will briefly introduce my research on a topos-theoretic approach to automata theory, which is based on the fact that the local state classifier of the category of word actions PSh(?*) is given by word congruences.

Operational Game Semantics (OGS) is a flexible method for building models for open terms based on their operational semantics. After motivating and giving a high-level overview of an OGS model, I will present the most important constructions from my PhD thesis. This will encompass: - a high-level axiomatization of abstract machines, used to build a (reasonably) language-generic OGS model, - a practical representation for programming with games and their strategies in intensional type theories such as Rocq, based on coinduction, - a high-level proof of the soundness of our generic OGS model w.r.t. contextual equivalence.

Ce séminaire exceptionnel, qui devrait intéresser absolument tous les membres de l'équipe LoCal, se déroulera dans un cadre original. Dans une première partie, nous présenterons les topos pour la logique linéaire en transportant des meubles d'un appartement balbynien dans un monospace. Dans une deuxième partie, nous analyserons la complexité de ces structures en transvasant ces mêmes meubles de ce même monospace dans un appartement idéalement situé à côté de Gare du Nord. Enfin, nous discuterons de la pertinence de notre approche socio-philosophique au cours d'un apéro dinatoire composé de bières et de pizzas (voire de vodkas) (en Coq)

In 1981, J. Kearns published 'Modal Semantics Without Possible Worlds' [1], in which he developed a semantics based on non-deterministic matrices for the modal logics KT, S4, and S5. Despite being an interesting alternative to the standard semantics, it does not provide a decision procedure. This problem remained open until recently, when L. Grätz [2] found a solution for KT and S4. Building on an extension of Kearns' semantics for modal logic K [3], we are now extending this solution to the entire normal modal cube. [1] Kearns, John T. "Modal semantics without possible worlds." The Journal of Symbolic Logic 46.1 (1981): 77-86. [2] Grätz, Lukas. "Truth tables for modal logics T and S4, by using three-valued non-deterministic level semantics." Journal of Logic and Computation 32.1 (2022): 129-157. [3] Omori, Hitoshi, and Daniel Skurt. "More modal semantics without possible worlds." IfCoLog Journal of Logics and their Applications 3.5 (2016): 815-846.

Skeletal Semantics is a meta-language to describe the semantics of programming languages. We present it through several examples, highlighting how complex features can be captured in a readable way using monads. These features range from simple effects like exceptions to more complex ones like generators.

Toposes are often motivated by presenting the special case of sheaves on a topological space. In general, a (Grothendieck) topos is constructed from a `site' consisting of a category equipped with a `Grothendieck coverage', so-called because in the motivating case the category involved is the partially ordered set of opens of a topological space and the coverage consists of the coverings of one open by its open subsets. In other words, the best-studied special case of sites are those where the underlying category is a poset. At the other extreme, when the underlying category is a monoid, a Grothendieck coverage becomes instead a collection of ideals closed under certain operations. In this talk we explain different ways in which the data of a Grothendieck coverage on a *free* monoid can be expressed, we explain how this is related to Cantor space(s) and to a certain equivalence relation on infinite words. Finally, we explain how this fits into our work on continuous actions of topological monoids (which some colleagues have already seen me talk about).

Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting successful techniques from Rust to higher-level languages, where they need to interact with other advanced features, especially various flavors of functional and type-level abstraction. In this talk, I will present reachability types, a recent proposal has shown promise in scaling lifetime reasoning to higher-order and polymorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. More specifically, I will present the simply-typed ??-calculus with precise lightweight (i.e., quantifier-free) reachability polymorphism, and the F<:?-calculus with bounded parametric polymorphism over types and reachability qualifiers. I will present meta-theory results, safe capability programming patterns enabled by reachability types, and flow-sensitive effect system extensions. If time permits, I will also discuss recent ongoing developments of reachability types.

Traditionally, computability theory is based on a notion of computable functions induced by concrete models like Turing machines, lambda calculus, or general recursion. While these models are well-studied, they only provide a somewhat secondary explanation of computability, at times obscuring the simple computational essence of abstract constructions and constituting a notorious burden for mechanisation in a proof assistant. In this talk, I will give an overview of synthetic computability theory as introduced by Richman and Bauer, offering an elegant alternative: at the price of giving up on some principles of classical reasoning, computability becomes a primitive notion, even internalisable by the axiom that every function is computable. After discussing this general framework in the context of constructive mathematics, I will describe some recent work on Gödel's incompleteness theorem and Post's problem, both developed synthetically in constructive type theory and mechanised in the Coq proof assistant.

Static resource analysis is dedicated to finding methods determining the quantify of resources (time, energy, memory, ...) required to run a program, together with the variables this quantity depends on. The cornerstone of this endeavour is finding invariants/variants between program states: an analyser must automatically understand the algorithms encoded into the program without programmer input. We will focus on resource analyses through type systems for functional languages. To this aim, we introduce AutoBill, an abstract machine used as intermediate representation for functional languages for resource analysis, both for monotone (energy, time) and non-monotone (memory, money) resources. We compile to this machine, amongst others, an ML-style language with data-structures (ADT), recursion (fixpoints), and some further extensions. AutoBill uses Call-by-Push-Value operational semantics, which mixes call-by-value and call-by-name, to encode the runtime semantics of functional languages. The use of an abstract machine furthermore allows continuations to be encoded as explicit call stacks. This in turns enables the re-use of data structures analyses to analyse control flow within programs. On top of our machine, a so-called polarized linear type system makes explicit the flow of resources that accompanies jumping in and out of computations. Those types are enriched with natural integer parameters, that are controlled during type-checking through the addition of equations and constraints to data-type definitions. This enables the approximating sizes, costs, combinatorial invariant, etc. in a first-order constraint. This is done during type-inference, and provides a link between those quantities and the largest resource usage occurring at runtime. The constraint is then sent to an SMT solver for validation, or to a linear programming optimizer to generate polynomial resource bounds. We implement the "Automated Amortized Resource Analysis" method in AutoBill. It assigns, to each data-structure, a count of the amount of sub-structures which relevant shapes. This is then used to bounds the iteration counts of an algorithm and obtain polynomial worst-case complexities. This implementation consists of a specialized compilation scheme from a source language to the abstract machine. The typing-and-analysis engine is then independent of both the source language and the chosen analysis method.