Rencontre, 19 octobre 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 call-by-name λ-calculus, is a congruence. This method has been adapted to call-by-value λ-calculus, PCF, λ-calculus with delimited continuations, higher-order π-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 memory-related bugs. However, the heap space usage of garbage-collected 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 high-level, yet sequential, language.
In this talk, we scale up to a concurrent language. For this purpose, we introduce new "pointed-by-thread" assertions, which keep track of the existence of stack-to-heap pointers in a reasonably lightweight manner. We illustrate our logic on several lock-free data structures, unveiling their subtle heap space usage.
- 15:15 – 16:15
-
Hugo Paquet (LIPN, Université Sorbonne Paris-Nord)
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 give the basic theory, and then discuss two results which demonstrate that element-free 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 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 models for clustering.
Joint work with Victor Blanchi.
