“Pour un entier positif n donné, on dénombre autant de partitions de n en parts distinctes que de partitions de n en parts impairs”.

Cette identité, attribuée à Euler, résume bien ce qu'est une identité du type Rogers-Ramanujan: une égalité entre cardinaux d'ensembles de partitions, qui pour l'un vérifient des conditions de congruences sur ses parts, et l'autre des conditions sur les différences entre parts consécutives.

Nous présenterons certaines méthodes utilisées pour établir ces égalités, telles que la méthode des mots pondérés, les équations de q-différence, ainsi que des bijections directes. On étudiera entre autre l'identié Alladi-Gordon qui généralise celle de Schur, et si le temps nous le permet, l'identité de Siladic issue de la théorie des représentations des algèbres de Lie.

Around the Curry-Howard correspondence, proof-theory has grown along two distinct fields: the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation.

This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in an overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two standard topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fr\'echet Nuclear spaces, and proofs are distributions with compact support. We show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Depuis leur introduction par Leray dans les années 50 les suites spectrales sont devenues essentielles dans beaucoup de domaines mathématiques comme outil de calculs homologiques et homotopiques. Parmi les sources importantes de suites spectrales on trouve les complexes filtrés et les bicomplexes. On introduit pour chacune de ces catégories la notion de E_r-quasi-isomorphisme, liée à la r-ième page des suites spectrales associées aux objets considérés. On montrera dans cet exposé, une fois toutes les notions utiles définies (y compris les structures de catégorie modèles) que les catégories des complexes filtrés et des bicomplexes admettent des structures de catégorie modèle au sens de Quillen, où les équivalences faibles sont les E_r-quasi-isomorphismes.

Ceci est un travail en commun avec: Joana Cirici, Daniela Egas-Santander et Sarah Whitehouse.

We study approximation algorithms for two closely related problems: the problems of finding a short synchronizing and a short mortal word for a given prefix code. Roughly speaking, a synchronizing word is a word guaranteeing a unique interpretation, and a mortal word is a word guaranteeing no interpretation for any sequence of codewords. We concentrate on the case of finite prefix codes and consider both the cases where the code is defined by listing all its codewords and where the code is defined by an automaton recognizing the star of the code. This is a joint work with Marek Szykuła (University of Wroclaw).

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.

This is joint work with Benedikt Bollig and Paul Gastin, presented at CONCUR’18.

A pattern in a permutation is a subsequence with a specific relative order. What can we say about a typical large random permutation that avoids a particular pattern? We use a variety of approaches. For certain classes we give a geometric description that relates these classes to other types of well-studied concepts like random walks or random trees. Using the right geometric description we can find the the distribution of certain statistics like the number and location of fixed points.

We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.