The most accessible way to visualize a (small) category is to consider its objects as vertices and its morphisms as oriented edges, forming some sort of graph. Polygraphs extend this intuition to form higher categories, where higher cells can be seen as oriented faces between edges, oriented solids between faces, &c. I will illustrate this construction with two families of categories, the oriented simplices and the oriented cubes, as well as showcase two operations that relate them when seen as constructed by a parametric language.

References:

Polygraphs: Dimitri Ara et al. Polygraphs: From Rewriting to Higher Categories.

Orientals: Ross Street. “The algebra of oriented simplexes” ; Dimitri Ara, Yves Lafont, and François Métayer. Orientals as free algebras.

Oriented Cubes: Iain R. Aitchison. The geometry of oriented cubes.

Parametricity: Hugo Herbelin and Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi- cubical sets.

Joint work with Shuo Li (U. Winnipeg) and Wolfgang Steiner (IRIF)

Hofstadter's G function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, a family $(F_k)$ of similar functions is obtained by varying the number $k$ of nested recursive calls in this equation. We present here a few nice properties of these functions. In particular, they can be described via some infinite morphic words generalizing the Fibonacci word. This was crucial for proving that this family is ordered pointwise: for all $k$ and $n$, $F_k(n) \le F_{k+1}(n)$. Moreover, these functions have a simple behavior on well-chosen numerical representations (Zeckendorf decompositions for some Fibonacci-like sequences). Thanks to that, we were also able to estimate the discrepancies for these $F_k$, i.e. the maximal distances between each $F_k$ and its linear equivalent. This whole work was formally proved using the Coq proof assistant (except for a beautiful fractal!) and we will give a gentle introduction to this Coq development.

Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In the work presented in this talk, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sens that we can exhibit such a controller.

Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability.

In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.

In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement.

Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability.

In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.

In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement.

For $(\lambda_{1},\dots,\lambda_{d})=\lambda\in(0,1)^{d}$ with $\lambda_{1}>\cdots>\lambda_{d}$, denote by $\mu_{\lambda}$ the Bernoulli convolution associated to $\lambda$. That is, $\mu_{\lambda}$ is the distribution of the random vector $\sum_{n\ge0}\pm\left(\lambda_{1}^{n},\dots,\lambda_{d}^{n}\right)$, where the $\pm$ signs are chosen independently and with equal weight. Assuming for each $1\le j\le d$ that $\lambda_{j}$ is not a root of a polynomial with coefficients $\pm1,0$, we prove that the dimension of $\mu_{\lambda}$ equals $\min\{ \dim_{L}\mu_{\lambda},d\} $, where $\dim_{L}\mu_{\lambda}$ is the Lyapunov dimension. This is a joint work with Ariel Rapaport.

In the last 50 years, the amount and complexity of information stored in databases has grown and the needs of database users have evolved. These changes have led to the creation of new models such as XML, key-value stores, time series databases and so on. The subject of this thesis is one such model: the graph database. In a graph database, data is stored as a “graph”, or a collection of nodes, representing the entities, connected together by edges, representing relationships between the entities. Additional information about the entities and their relationships can be attached to the nodes and edges. This powerful model, popularized by Neo4j in 2010, is now a staple in various industries such as biology, social networks and banking. By putting the links between the data points front and center, graph databases allow users to reason not only about individual elements but also about the structure of the graph. Accordingly, the goal of a typical graph query is to find a “path” connecting specific nodes.

Because graph traversals inherently rely on transitivity, traditional query languages are not suitable in the graph context, and thus new languages have been created. In the theoretical community, the basic building blocks of a graph language are the Regular Path Queries (RPQs), which define path constraints by way of regular expressions. The expressive power and complexity of RPQs and their extensions (by union, conjunction, two-way navigation, data value comparisons and path properties for example) have been studied since the 1990s but their properties are barely beginning to be understood.

The most popular practical graph language today is Neo4j’s Cypher. In Cypher, a path can be described by a regular expression but it also includes many other features among which aggregation, different path semantics, projection, subqueries and updates. These elements differ from those of other languages, like Tigergraphs’ GSQL, or Oracle’s PGQL, but all graph systems share the same kernel: pattern matching.

In 2019, a new International Organisation for Standardization (ISO) group was created to oversee the standardization of practical graph languages. This led to two new standards: SQL/PGQ and GQL. The idea of SQL/PGQ is to add a view-based pattern matching mechanism to SQL and interpret the relational data as a graph only when necessary, whereas GQL is standalone and stores the data as a native graph. While this standardization work is a step in the right direction, there is one crucial ingredient missing: a corresponding theoretical model.

The goal of this thesis is to define a theoretical language for graph databases, akin to relational algebra for SQL, that reflects the essential aspects of GQL and SQL/PGQ while being simple enough for theoretical study. We start by presenting in detail the pattern matching features shared by SQL/PGQ and GQL. We then identify and formalize the core of this language. Afterwards, we position our formalisations of SQL/PGQ and GQL in comparison to relational algebra, which allows us to highlight their distinct styles, while also proving their equivalence. Finally, we explore the impact of extending pattern matching with list functions and show that this addition is not only dangerous in theory, but also fails in practice.