Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Séminaires
Agenda
Séminaires antérieurs
Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Speaker: Nicolas Magaud, IGG, Université de Strasbourg.
Thursday 14 April 2022, 11:00, (room 1Z61 ENS Paris-Saclay and online)
Abstract: We formally implement the smallest three-dimensional projective space PG(3,2) in the Coq proof assistant. This projective space features 15 points and 35 lines, related by an incidence relation. We define points and lines as two plain datatypes (one with 15 constructors for points, and one with 35 constructors for lines) and the incidence relation as a boolean function, instead of using the well-known coordinate-based approach relying on GF(2)^4. We prove that this implementation actually verifies all the usual properties of three-dimensional projective spaces. We then use an oracle to compute some characteristic subsets of objects of PG(3,2), namely spreads and packings. We formally verify that these computed objects exactly correspond to the spreads and packings of PG(3,2). For spreads, this means identifying 56 specific sets of 5 lines among 360 360 (= 15 x 14 x 13 x 12 x 11) possible ones. We then classify them, showing that the 56 spreads of PG(3,2) are all isomorphic whereas the 240 packings of PG(3,2) can be classified into two distinct classes of 120 elements. Proving these results requires partially automating the generation of some large specification files as well as some even larger proof scripts. Overall, this work can be viewed as an example of a large-scale combination of interactive and automated specifications and proofs. It is also a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).
Hazel: a Separation Logic for effect handlers
Speaker: Paulo de Vilhena, Inria Paris.
Tuesday 19 April 2022, 11:00, (room 1Z31 ENS Paris-Saclay and online)
Abstract: A program logic is a pair of a language, for writing specifications, and a set of reasoning rules, for deriving specifications. In this talk, I present Hazel, a program logic for effect handlers. I start by laying out the motivation for such work and then I present its main ideas: how to write the specification of effectful programs in Hazel and what reasoning principles does it suggest? Finally, I apply these ideas to `invert`, a function that exploits effect handlers to produce a lazy sequence (a cascade) out of a higher-order iteration function.
Avoiding deadlocks in lock-sharing systems
Speaker: Corto Mascle, LaBRI.
Tuesday 12 April 2022, 11:00, (room 1Z71 ENS Paris-Saclay and online)
Abstract: We consider the distributed control problem for systems with locks. We introduce a model in which some processes running in parallel cannot communicate directly, but may acquire or release some shared locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable, but in this talk we will focus on systems in which each process can access at most two locks. The problem then becomes complete for the second level of the polynomial hierarchy, and even in PTIME under some additional assumptions. The dining philosophers problem satisfies these assumptions.
The relational semantics, and beyond
Speaker: Giulio Manzonetto, LIPN.
Tuesday 19 April 2022, 10:00, (room 1Z71 ENS Paris-Saclay and online)
Abstract: Since the pioneering work by Barendregt, Dezani-Ciancaglini and Coppo, some models of lambda-calculus are based on filters and can be presented as intersection type systems. The interpretation of a program in these models is just the set of its types, which is a filter. Filter models can be used to capture operational properties of programs like normalization, head normalization, or solvability, but establishing these results often requires impredicative techniques like Girard's reducibility candidates. In this talk we present a more recent class of models, called relational models and arising from a simple quantitative semantics of linear logic (LL). We show that these models can be presented as intersection type systems where the intersection operator is however non-idempotent. Due to the resource sensitive nature of LL , we are able to capture operational properties bypassing impredicative techniques. Starting for the type of a program, it is indeed possible to extract an upper bound to the amount of steps needed to reach its value. We will see that generalizing this semantics from the Boolean semiring to continuous semi-ring allows to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF). Finally, generalizing relations to the higher-dimension (profunctors) allows us to obtain the characterization of the theory of a model as a simple corollary of the Approximation Theorem.
Formal Verification of Finite Systems: Contributions and Adoption to security properties
Speaker: Kais Klai, LIPN, Université Sorbonne Paris Nord.
Monday 11 April 2022, 11:00, (room 1Z25 ENS Paris-Saclay and online)
Abstract: In this talk, I will present different variants of an hybrid graph structure called Symbolic Observation Graph (SOG) that preserves stutter-invariant temporal properties of finite systems. The SOG is an explicit graph where nodes are encoded symbolically with decision diagram techniques and allows on-the-fly LTL model checking. Despite its theoretical exponential complexity, it reduces in practice the state space explosion problem and performs better than explicite and symbolic exhaustive verification approaches. The second part of the talk illustrates the adoption of such a graph for the verification and the supervision of the opacity property. Finally, I will introduce a current work on model checking of vulnerability and specific properties of Blockchain smart contracts -based processes.
Electronic voting: design, attacks and proofs
Speaker: Véronique Cortier, Loria
Tuesday 14 December 2021, 11:00, (1Z56, bât ENS)
Abstract: Electronic voting aims to achieve the same properties as traditional paper based voting. Even when voters vote from their home, they should be given the same guarantees, without having to trust the election authorities, the voting infrastructure, and/or the Internet network. The two main security goals are vote privacy: no one should know how I voted; and verifiability: a voter should be able to check that the votes have been properly counted.
In this talk, we will present the Belenios voting platform, its security properties and its limitations. On a more theoretical side, we will see how recent techniques allow to compute exactly the result of an election (e.g. the winners) without leaking information about the set of ballots. Such techniques are based on Multi-Party Computations (MPC).
Structures from Quantum Relations
Speaker: Titouan Carette
Friday, 16 December 2022, 11:00, 1Z77
Abstract: The category of relations and the category of complex linear maps have a lot in common. In particular, they are both compact closed. More concretely, in the same way that any classical process can be characterized by its set of admissible behaviours, any quantum process can be characterized by one vector, a quantum state over all observable behaviours. Thus, complex vectors can be thought of as the quantum generalization of the concept of relations. In this talk, I will illustrate this quantum relation paradigm with two examples. First, I will present a model of quantum wang tiles able to represent quantum configurations obeying local constraints. Then I will outline applications to the semantics of quantum processes via a model of generalized proof nets. Finally, I will provide arguments for the extension of those approaches beyond the quantum realm.
Sleeping is Superefficient: MIS in Exponentially Better Awake Complexity
Speaker: Fabien Dufoulon
Friday, 16 December 2022, 14:00, 1Z77
Abstract:
Maximal Independent Set (MIS) is one of the fundamental and most well-studied problems in distributed graph algorithms. Even after four decades of intensive research, the best-known (randomized) MIS algorithms have O(log n) round complexity on general graphs [Luby, STOC 1986] (where n is the number of nodes), while the best-known lower bound is Ω(√(log(n)/log(log n))) [Kuhn, Moscibroda, and Wattenhofer, JACM 2016]. Breaking past the O(log n) bound or showing stronger lower bounds have been longstanding open problems.
Characterising one-player positionality for infinite duration games on graphs
Speaker: Pierre Ohlmann, IRIF
Tuesday 30 November 2021, 11:00, (Salle 1Z56, bât ENS)
Abstract: I will present a new result, asserting that a winning condition (or, more generally, a valuation) which admits a neutral letter is positional over arbitrary arenas if and only if for all cardinals there exists a universal graph which is monotone and well-founded. Here, "positional" refers only to the protagonist; this concept is sometimes also called "half-positionality".
This is the first known characterization in this setting. I will explain the result, quickly survey existing related work, show how it is proved and try to argue why it is interesting.
Routed quantum circuits
Speaker: Augustin Vanrietvelde, Imperial College London
Tuesday 23 November 2021, 11:00, (Salle 1Z31, ENS Paris-Saclay)
Abstract: I will present the results of a recently published paper. In this paper, we argue that the quantum-theoretical structures studied in several recent lines of research cannot be adequately described within the standard framework of quantum circuits. This is in particular the case whenever the combination of subsystems is described by a nontrivial blend of direct sums and tensor products of Hilbert spaces. We therefore propose an extension to the framework of quantum circuits, given by routed linear maps and routed quantum circuits. I will outline the application of this formalism to the problem of the coherent control of quantum channels, and a potential application to the study of indefinite causal order.