There are well-known dualities of computation in both functional and concurrent programming: input/output, expression/context, strict/lazy, sender/receiver, forward/backwards, and several others. When viewed through an algebraic lens, these can be understood as metaphysical interpretations of rigorous mathematical dualities.

In this talk, I will explore the duality of values and continuations (Filinski'89) through the lens of cartesian closure/co-cartesian co-closure. The main observation is that, just as higher-order functions give exponentials, higher-order continuations give co-exponentials. Using this semantic duality, I will present a λλ~ (lambda-lambda-bar or tilde) calculus, which exhibits a duality of abstraction/co-abstraction. I will develop the syntax and semantics of this language, which gives a computational interpretation in terms of speculative execution and backtracking.

Using this language, I will show how to recover classical control operators, the computational interpretation of classical logic, and a complete axiomatisation of control effects. Finally, I will show how this dualises Lambek's functional completeness, thereby dualising Hasegawa's decomposition of λ-calculus into first-order κ/ζ-calculi.

A classical result in concurrency theory shows that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide a characterisation of the deterministic computations of a net via monoidal categories, accounting for their sequential and parallel composition. In turn, this characterisation leads to the interpretation of such computations as sequents of the multiplicative fragment of linear logic. The talk presents a survey of the topic, including recent results concerning non-deterministic computations and their characterisation in terms of dioidal categories, the categorical equivalent of tropical semirings, as well as suggesting a possible connection with the multiplicative additive fragment of linear logic.

I will give an introduction to directed algebraic topology and its application in concurrency theory, covering directed spaces, directed paths, and directed homotopies. Then I will touch upon the combinatorial side of things, precubical sets and higher-dimensional automata (HDAs), which will bring us to the second part of the talk: the language theory of HDAs. This makes the connection back to the initial motivation, concurrency theory, and also gives new inspiration and tools to directed topology.

Software sciences have a role to play in the description, the organization, the execution, and the analysis of the molecular interaction systems such as biological signaling pathways. These systems involve a huge diversity of bio-molecular entities whereas their dynamics may be driven by races for shared resources, interactions at different time- and concentration-scales, and non-linear feedback loops. Understanding how the behavior of the populations of proteins orchestrates itself from their individual interactions, which is the holy grail on systems biology, requires dedicated languages offering adapted levels of abstraction and efficient analysis tools.

In this talk we describe the design of formal tools for Kappa, a site-graph rewriting language inspired by bio-chemistry. In particular, we introduce a static analysis to compute some properties on the biological entities that may arise in models, so as to increase our confidence in them. We also present a model reduction approach based on a study of the flow of information between the different regions of the biological entities and the potential symmetries. This approach is applied both in the differential and in the stochastic semantics.

To better understand Barendregt's genericity for the untyped call-by-value lambda-calculus, we start by first revisiting it in call-by-name, adopting a lighter statement and establishing a connection with contextual equivalence. Then, we use it to give a new, lighter proof of maximality of head contextual equivalence, i.e. that H* is a maximal consistent equational theory. We move on to call-by-value, where we adapt these results and also introduce a new notion dual to light genericity, that we dub co-genericity. We present light (co-)genericity as robust properties rather than just lemmas and provide different proofs based on applicative bisimilarity, semantic models and direct rewriting techniques.

CompCert is the only formally-verified C compiler, and one of the very few formally verified compilers altogether. It is intended for use for safety-critical applications. I will discuss some improvements we implemented over CompCert: new VLIW target, new optimizations, and security features. A lot of our development uses untrusted oracles implemented in OCaml plus a formally verified checker. I will discuss typing issues regarding this interface and some questions we have about them.

Over the past 5 to 10 years, machine learning has revolutionised program synthesis. In this talk we'll present ProgSynth, a general purpose program synthesis tool based on neurosymbolic methods. We'll discuss some challenges: combinatorial search, semantic program synthesis, and reinforcement learning.

A first such link appeared in the context of previous work, in which we provided an algebraic formalisation of categorical coherence theorems in higher dimensional analogs of Kleene algebras. I will briefly recall our definition of the latter and the associated coherence theorems. However, this link between categorical and algebraic structures has since led us to a Jónsson-Tarski correspondance between (higher) catoids, generalizations of (higher) categories, and (higher) quantales. The latter were introduced as a non-commutative extension of locales, and have since also been studied in the context of categorical logic. The first part of this talk will focus on this correspondance and its extension to the associated convolution algebras. These results, as well as the coherence theorem described above, have been formalized in the proof assistant Isabelle.

In the second part of this talk, I will describe ongoing work relating rewriting, quantales, and (directed) topological methods. The goal of this work is to describe the congruences of multinomial lattices and their continuous analogs, in particular the quantale Qv(I) of sup-continuous endomorphisms of the ordered unit interval. The former, generalizing the permutohedra, provide a description of the rewriting system associated to commutativity on finite words, while the latter are studied in the context of categorical linear logic. These structures all have an interpretation as directed spaces, the homotopy types of which are closely related to their congruences. I will describe this correspondance, and briefly discuss the use of topological duality in our ongoing study of these structures.

An “element-free” probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, in situations where the specific identity of elements is not important. This talk is about the theory of element-free distributions in the category of measurable spaces. I will explain the basic concepts, and then present two new results which demonstrate that element-free distributions are a canonical notion. The first result is a categorical version of a representation theorem for random partitions, originally due to Kingman, which characterises the space of element-free distributions as a limit in the Kleisli category for the Giry monad G. The second result establishes a correspondence between random element-free distributions and natural transformations of type G → GG. I will sketch the relevance of this theory to nonparametric Bayesian clustering.

This is joint work with Victor Blanchi.