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.

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

6th French-Israeli Workshop on Foundations of Computer Science


27 novembre 2017 · Salle 3052 (Sophie Germain)

Journée du pôle Automates, Structures, et Vérification


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

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


lundi 27 novembre 2017 · 14h00 · Salle des Thèses, Halle aux Farines

Soutenance d'habilitation · Stefano Zacchiroli (IRIF) · Large-scale Modeling, Analysis, and Preservation of Free and Open Source Software


mardi 28 novembre 2017 · 10h30 · Salle 3052

Sémantique · Daniela Petrisan (IRIF) · TBA


mardi 28 novembre 2017 · 14h00 · Salle 3052

Analyse et conception de systèmes · Leon Gondelman (Institute for Computation and Information Sciences (Radboud Univ.), Netherlands) · The Spirit of Ghost Code

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.


mardi 28 novembre 2017 · 13h30 · Salle 3052

Vérification · Léon Gondelman (Radboud University, The Netherlands) · The Spirit of Ghost Code

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge.

The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.