Together with Fixed Priority Scheduling, Earliest Deadline First (EDF) is the second leg on top of which a large portion of the research on real-time systems stands. At the heart of the EDF exact schedulability test, a pivotal role is played by the demand bound function test, which requires to evaluate whether the amount of work required to complete a set of jobs is less than or equal to the amount of time available. Such a test is checked over a set of time instants.

In this work, it is proposed a method that cuts drastically the set of constraints to be checked. Such a method is applicable also to tasks with release offset. Notably, it is proved that such a reduced set of constraints is minimal: it is not possible to reduce the set any further without losing the sufficiency of the test. The code to make this reduction is publicly available on GitHub.

Twenty-five years ago, Kaplan and Tarjan established a striking result: there exist “purely functional, real-time deques with catenation”. In other words, there exists a data structure that supports the following operations: “push” and “pop” which insert and extract one element at the front end, “inject” and “eject” which insert and extract one element at the rear end and “concat”, the concatenation operation. Moreover, the data structure is persistent: none of the five operations modifies or destroys its argument. Finally, each operation has worst-case time complexity O(1). This presentation will provide an overview of the first ever implementation of the data structure, done in OCaml, and its verification in Rocq.

Back in 1939, Frucht proved that every finite group is isomorphic to the automorphism group of a finite graph. This incited an examination of the influence that standard graph theoretical concepts can have on automorphism groups. Eventually, the framework was enlarged by extending the analyses to endomorphism monoids. This has ultimately established a particular connection between semigroup classes and graph classes, notably in terms of sparsity and combinatorial regularity. The goal of the presentation is to contextualize a new result on endomorphism monoids of regular graphs that adds some detail to the picture. This is joint work with Kolja Knauer.

Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyễn but focusing on edge-colored graphs instead of perfect matchings.

[Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair]

Decimal writing is just one way of notating the natural numbers, but we can as well consider the “first” ways of doing so: unary writing (the tally system), binary writing (the language of classical computers) or even ternary writing (examples welcomed!). Unary gives a natural labelling on the family of simplices (the family to which belongs the triangle, the tetrahedron,…) and furthermore a way of orienting any dimensional face of such shapes. Likewise, binary is the natural choice to label and orient the family of cubes (the square, the cube,…). In this talk I will show these constructions, as well as how this particular labelling allows us to easily construct simplices from cubes and cubes from simplices. Lastly, I will address the elephant in the room: what gets labelled and oriented by ternary ?!

There are no prerequisites for the content of this talk more than a basic understanding of binary, however these ideas come from higher category theory and type theory, in particular work by Street and Aitchison on the oriented simplices and cubes respectively, as well as work by Ara, Lafont and Métayer to better uncover these constructions, and the notion of parametricity as presented by Herbelin and Ramachandra.

The model, due to Jurdzinski in his PhD thesis 1999 under the direction of Kutylovski, is a finite collection of one-way or two-way deterministic automata working synchronously on the same input and dispatching messages when reaching certain so-called broadcasting states. The input is accepted if a predetermined automaton reaches a final state when it arrives at the right end of the input. The message complexity of the system is the function f(n) which, to every integer, assigns the minimum number of messages required in a run over inputs of length n.

Jurdzinski and Kutylovski, 2002, proved in the one-way case that if the system requires a nonconstant number of messages then it requires at least log(n) messages and claimed a result of the same kind for two-way systems.

I show that when the input is unary, i.e., over an alphabet with a unique letter, the language accepted is rational (or equivalently ultimately periodic) if and only if the number of messages is finite.

The connection between logic and computer science has been fruitfully explored for years, and yet there is still so much to uncover. This thesis aims to further enrich this fascinating field by delving into the interplay between the ecosystem of linear logic and that of programming languages. In the first part, we introduce a new definition of parallel cut elimination for multiplicative-exponential linear logic (MELL) proof nets. Drawing inspiration from Tait and Martin-Löf’s parallel reduction in the lambda calculus, we address the challenges posed by untyped proof nets by defining a generalized notion of substitution on more abstract structures called prestructures. This approach allows us to define parallel exponential cut elimination for MELL prestructures in a rigorous and systematic way. Through the strong confluence of this operation, we provide a confluence proof for cut elimination in MELL proof nets without relying on Newman’s lemma or strong normalization. Furthermore, we extend this framework to define complete parallel cut elimination, offering an alternative confluence proof that closely mirrors Tait and Martin-Löf’s approach for the lambda calculus. The second part of this work introduces a new logic system, PiL, which extends first-order multiplicative and additive linear logic by incorporating a non-commutative, non-associative connective and nominal quantifiers. We prove that PiL enjoys cut elimination and embed the recursion-free fragment of the pi-calculus within PiL, demonstrating that the operational semantics of the pi-calculus can be captured by linear implication in PiL. This result allows us to characterize key properties such as deadlock freedom, ensuring that a network of processes can continue executing until termination, and progress, particularly for systems without mobility.Additionally, we establish a choreographies-as-proofs correspondence, providing the first completeness theorem for choreographies within this fragment of the pi-calculus. Finally, we introduce proof nets for PiL by integrating techniques from conflict nets and unification nets, thereby defining the first syntax for conflict nets in the context of multiplicative-additive linear logic with first-order quantifiers. By linking computation trees to derivations and deriving canonical representatives of these trees in the same manner as proof nets represent sequent calculus proofs, this work opens new avenues for bridging computation and logic.

A clone on a set is a family of finitary operations on the set that is closed under projections and composition. Abstract clones are the algebras for the many-sorted equational presentation that axiomatises this structure. Categorically, they are (finitary, one-sorted) algebraic theories. Inspired by works in algebraic logic, we shall define an equational class of abstract clones, tentatively dubbed “partition clones'', and describe some of their properties; in particular, we will show that this family of abstract clones has lot in common with Boolean algebras. Among the results we shall present, there is a theorem concerning the lattice of hypervarieties (i.e. varieties of abstract clones) already proven in 1991 by George M. Bergman from a different perspective. We shall explain the link between his approach and ours.

In the realm of integer factorization, certain methods, such as CFRAC, leverage the properties of continued fractions, while others, like SQUFOF, combine these properties with the tools provided by quadratic forms. Recently, Michele Elia revisited the fundamental concepts of SQUFOF, including reduced quadratic forms, distance between quadratic forms, and Gauss composition, offering a new perspective for designing factorization methods.

In this seminar, we present our algorithm, which is a refinement of Elia's method, along with a precise analysis of its computational cost. Our algorithm is polynomial-time, provided knowledge of a (not too large) multiple of the regulator of $\mathbb{Q}(\sqrt{N})$. The computation of the regulator governs the total computational cost, which is subexponential, and in particular $O(\exp(\frac{3}{\sqrt{8}}\sqrt{\ln N \ln \ln N}))$. This makes our method more efficient than CFRAC and SQUFOF, though less efficient than the General Number Field Sieve.

We identify a broad family of integers to which our method is applicable including certain classes of RSA moduli. Finally, we introduce some promising avenues for refining our method. These span several areas, ranging from Algebraic Number Theory, particularly for estimating the size of the regulator of $\mathbb{Q}(\sqrt{N})$, to Analytic Number Theory, particularly for computing a specific class of $L$-functions.

Joint work with Nadir Murru.