Rencontre, Oct. 19, 2023
Programme
 10:30 – 12:00

Tom Hirschowitz (CNRS, Université Savoie Mont Blanc)
Research in programming languages mostly proceeds language by language. This in particular means that key ideas are often introduced for one typical language, and must then be adapted to other languages.
A prominent example of this is Howe's method for proving that applicative bisimilarity, a notion of program equivalence in callbyname λcalculus, is a congruence. This method has been adapted to callbyvalue λcalculus, PCF, λcalculus with delimited continuations, higherorder πcalculus,…
In this work, using category theory, we establish an abstract congruence theorem for applicative bisimilarity, of which most existing adaptations of Howe's method are instances. The framework is both simpler and more general than our previous attempts.
This is joint work with Ambroise Lafont.
 13:45 – 14:45

Alexandre Moine (Cambium, INRIA)Invited talk: Diamonds Are Forever: Reasoning about Heap Space in a Concurrent and Garbage Collected Language
Memory management is notoriously difficult in a concurrent setting. The presence of garbage collection greatly simplifies the life of the programmer, eradicating many memoryrelated bugs. However, the heap space usage of garbagecollected programs can be tricky to understand and reason about, as there is no explicit program point where space is reclaimed.
We recently presented a Separation Logic with Space Credits to reason about heap space under garbage collection in a highlevel, yet sequential, language.
In this talk, we scale up to a concurrent language. For this purpose, we introduce new "pointedbythread" assertions, which keep track of the existence of stacktoheap pointers in a reasonably lightweight manner. We illustrate our logic on several lockfree data structures, unveiling their subtle heap space usage.
 15:15 – 16:15

Hugo Paquet (LIPN, Université Sorbonne ParisNord)
An "elementfree" 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 elementfree distributions in the category of measurable spaces. I will give the basic theory, and then discuss two results which demonstrate that elementfree distributions are a canonical notion. The first result is a new categorical version of a representation theorem for random partitions, originally due to Kingman, which characterises the space of elementfree distributions as a limit in the Kleisli category for the Giry monad G. The second result establishes a correspondence between random elementfree distributions and natural transformations of type G → GG. I will sketch the relevance of this theory to nonparametric models for clustering.
Joint work with Victor Blanchi.