Institut de Recherche en Informatique Fondamentale

IRIF CNRS Université Paris-Diderot

L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot.

Les objectifs scientifiques de l'IRIF se situent au cœur de l'informatique, se focalisant sur la conception, l'analyse, la preuve et la vérification d'algorithmes et de programmes, appuyé sur des recherches fondamentales en combinatoire, théorie des graphes, logique, automates, etc.

14 novembre 2017 · 11h · Salle des thèses, Halle aux Farines

Soutenance de thèse · Gabriel Radanne


17 novembre 2017 · 15h15 · Salle 153, Olympe de Gouges

Soutenance de thèse · Étienne Miquey


20 novembre 2017 · 10h · Salle 227C, Halle aux Farines

Soutenance d'habilitation · Paul-André Melliès


27 novembre 2017 · 14h · Salle des thèses, Halle aux Farines

Soutenance d'habilitation · Stefano Zacchiroli


November 22-23, 2017 · Tel-Aviv University, Israel

6th French-Israeli Workshop on Foundations of Computer Science


1er décembre 2017 · 14h30 · Salle des thèses, Halles aux Farines

Soutenance de thèse · Maxime Lucas


December 8, 2017 · Room 3052, IRIF

1st IQC-IRIF Workshop on Quantum Information Processing


October 7-9, 2018 · Maison de la Chimie, Paris

59th IEEE Symposium on Foundations of Computer Science (FOCS 2018)


Archives

lundi 20 novembre 2017 · 11h00 · Salle 1007

Vérification · Laurent Fribourg (LSV, CNRS & ENS de Cachan) · Euler’s Method Applied to the Control of Switched Systems

Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthezing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler’s method is the most basic technique for approximating such solutions. We present here an estimation of the Euler’s method local error, using the notion of “one-sided Lispchitz constant’’ for modes. This yields a general synthesis approach which can encompass uncertain parameters, local information and stochastic noise.

We will sketch out how the approach relates with other symbolic methods based on interval arithmetic and Lyapunov functions. We will also present some applicative examples which illustrate its advantages and limitations.


mardi 21 novembre 2017 · 11h00 · Salle 1007

Algorithmes et complexité · André Chailloux (INRIA Paris) · A tight security reduction in the quantum random oracle model for code-based signature schemes

Quantum secure signature schemes have a lot of attention recently, in particular because of the NIST call to standardize quantum safe cryptography. However, only few signature schemes can have concrete quantum security because of technical difficulties associated with the Quantum Random Oracle Model (QROM). In this paper, we show that code-based signature schemes based on the full domain hash paradigm can behave very well in the QROM i.e. that we can have tight security reductions. We also study quantum algorithms related to the underlying code-based assumption. Finally, we apply our reduction to a concrete example: the SURF signature scheme. We provide parameters for 128 bits of quantum security in the QROM and show that the obtained parameters are competitive compared to other similar quantum secure signature schemes.

Joint work with Thomas Debris-Alazard


mardi 21 novembre 2017 · 10h30 · Salle 3052

Sémantique · John Baez (UCLA Riverside) · Compositionality in Network Theory

To describe systems composed of interacting parts, scientists and engineers draw diagrams of networks: flow charts, Petri nets, electrical circuit diagrams, signal-flow graphs, chemical reaction networks, Feynman diagrams and the like. In principle all these different diagrams fit into a common framework: the mathematics of symmetric monoidal categories. This has been known for some time. However, the details are more challenging, and ultimately more rewarding, than this basic insight. Two complementary approaches are presentations of symmetric monoidal categories using generators and relations (which are more algebraic in flavor) and decorated cospan categories (which are more geometrical). In this talk we focus on the latter.


mercredi 22 novembre 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Jules Chouquet (Proofs and Programs team) · Linear logic proof nets and Taylor expansion.

I will first introduce linear logic proof nets, for the multiplicative and exponential fragment (MELL), and I will especially insist on the computational meaning of the exponential boxes: these are constructions containing the possibility of duplication and deletion of entire parts of the structures (all the non linear part of the calculus).

Once these notions are introduced, I will explain how it is possible to express this computational paradigm in a linear setting through a syntactical Taylor expansion. The idea is to understand exponential boxes in a differential variant of linear logic, and to represent it with linear combination.

If we have time, I will try to give an idea of some algebraic issues concerning this construction, and a method to show for example, that the normal form of the Taylor expansion of a MELL always converges.

NB: Taylor expansion is here analogical to the lambda calculus (with its differential version too) one, if someone heard about it, it can give a first intuition.


jeudi 23 novembre 2017 · 11h45 · Salle 1007

Combinatoire énumérative et analytique · Mathias Lepoutre (École Polytechnique (LIX)) · A bijective proof of the enumeration of maps in higher genus

Bender and Canfield proved in 1991 that the generating series of maps in higher genus is a rational function of the generating series of planar maps. In this talk, I will give the first bijective proof of this result. Our approach starts with the introduction of a canonical orientation that enables us to construct a bijection between $4$-valent bicolorable maps and a family of unicellular blossoming maps.


jeudi 23 novembre 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Simon Castellan (Imperial College) · The parallel intensionally fully abstract model for PCF

In this talk, we introduce a new game semantics framework for concurrency based on event structures, extending the work of Rideau and Winskel. In this framework, we can extend the notions of innocence and well-bracketing to the concurrent (and non-deterministic) case, generalizing the so-called “Abramsky cube”.

This talk focuses on the deterministic case. I will first introduce the concurrent strategies and their composition, in the existing linear setting. I will then present our extension to nonlinearity using copy indices and symmetry to represent uniformity. I will then present our notions of concurrent innocence & well-bracketing, to finish on our result of intensional full abstraction for PCF. Time permitting, I will discuss extensions of this result to non-angelic nondeterminism and probabilities.


vendredi 24 novembre 2017 · 14h30 · Salle 3058

Automates · Paul Brunet (University College London) · tba