PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations.

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

Collaboration avec Rigo Florez. Nous généralisons la définition de l'activité à un cadre plus large contenant les matroides et des arbres enracinés. Ceci était motivé par un problème concernant l'arrangement de Linial.

Timed automata, as their name suggests, are a kind of automata in which time is taken into account. This is done by the presence of a number of clocks which can be tested or reset. Ever since they were introduced by Rajeev Alur and David L. Dill, they have been very important for modelling real-time systems. This presentation will give an introduction to the topic of timed automata, as well as present some usual tools and concepts for analysing them. Among these is the notion of clock regions, which spawn a very visual way of understanding the behaviour of these automata, and which will allow to state Puri's result characterizing reachability for a path.

Time permitting, I will talk about how starting from these tools, with some necessary additional work, it was possible to establish a characterization of the amount of “information per time unit” generated by a given automaton. This notion of “information” is to be defined during the presentation, it is the one we introduced recently, inspired by Kolmogorov and Tikhomirov's notion of epsilon-entropy.

Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull.

This talk is on joint work with J. Bell.

We study the computational complexity of finding a solution in straight-cut and square-cut pizza sharing, where the objective is to fairly divide 2-dimensional resources. We show that, for both the discrete and continuous versions of the problems, finding an approximate solution is PPA-complete even for very large constant additive approximation, while finding an exact solution for the square-cut problem is FIXP-hard and in BU. We also study the corresponding decision variants of the problems and their complexity. All our hardness results for the continuous versions apply even when the input is very simple, namely, a union of unweighted squares or triangles.

Joint work with Argyrios Deligkas and John Fearnley.

We study the computational complexity of finding a solution in straight-cut and square-cut pizza sharing, where the objective is to fairly divide 2-dimensional resources. We show that, for both the discrete and continuous versions of the problems, finding an approximate solution is PPA-complete even for very large constant additive approximation, while finding an exact solution for the square-cut problem is FIXP-hard and in BU. We also study the corresponding decision variants of the problems and their complexity. All our hardness results for the continuous versions apply even when the input is very simple, namely, a union of unweighted squares or triangles.

Joint work with Argyrios Deligkas and John Fearnley.

Generalised Mycielskians of odd cycles are relatively small graphs with high odd girth and chromatic number 4. In the literature there are many proofs using different techniques, like methods from algebraic topology, to show the second property. It is also proven by DeVos et al that these graphs have circular chromatic number 4. Using a result from about the same time of Simonyi and Tardos, namely that for a “topologically t-chromatic” graph $G$, where $t$ is even we have $\chi_c(G) = \chi(G) = t$, one can also get this strengthened statement.

In this talk we present a new, relatively short direct proof for the circular chromatic number, using only a basic notion of algebraic topology, namely the winding number. Then we present another graph family with high odd girth and circular chromatic number 4. This construction is very similar to the generalized Mycielski, but on its first two layers it forms a M$\ddot{o}$bius ladder. We prove the statement about their circular chromatic number with similar techniques. Moreover we present a similar result for a family of signed graphs.

This talk is based on a joint work with Reza Naserasr (Universit´e de Paris, IRIF, CNRS, F-75006, Paris, France), S Rohini (Indian Institute of Technology Madras, India) and S Taruni (Indian Institute of Technology Dharwad, India).

https://arxiv.org/abs/2301.00194

Given two finite automata A1, A2, recognising languages L1, L2, respectively, the state complexity of union (or intersection, or complement, etc.) is how many states (in terms of the number of states in A1, A2) may be needed in the worst case for an automaton that recognises L1 union L2 (or L1 intersect L2, or the complement of L1, etc.). The state complexity of complementing unambiguous finite automata has long been open, and as late as 2015 Colcombet asked whether unambiguous automata can be complemented with a polynomial blowup. I will report on progress on this question in recent years, both in terms of lower and upper bounds. For the currently best lower bound, techniques from communication complexity play an essential role.