Institut de Recherche en Informatique Fondamentale

IRIF Université Paris 7 CNRS L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot, issue de la fusion des deux UMR LIAFA et PPS au 1er janvier 2016.

Ses objectifs scientifiques se déclinent selon trois grandes thématiques au cœur de l'informatique : les fondements mathématiques de l’informatique ; les modèles de calcul et de preuves ; la modélisation, les algorithmes et la conception de systèmes.


Jeudi 12 et vendredi 13 octobre 2017 · Salle 3052

Journées de rentrée PPS

Lundi 6 novembre 2017 · Amphi Turing

Journée d'accueil des nouveaux membres de l'IRIF

Prochains séminaires

vendredi 20 octobre 2017 · 14h30 · Salle 3058

Automates · Sylvain Perifel (IRIF) · Lempel-Ziv: a “one-bit catastrophe” but not a tragedy

The robustness of the famous compression algorithm of Lempel and Ziv is still not well understood: in particular, until now it was unknown whether the addition of one bit in front of a compressible word could make it incompressible. This talk will answer that question, advertised by Jack Lutz under the name “one-bit catastrophe” and which has been around since at least 1998. We will show that a “well” compressible word remains compressible when a bit is added in front of it, but some “few” compressible words indeed become incompressible. This is a joint work with Guillaume Lagarde.

lundi 23 octobre 2017 · 11h00 · Salle 1007

Vérification · Raphaël Caudelier (IRIF - Université Paris Diderot) · FocaLiZe and Dedukti to the Rescue for Proof Interoperability

Numerous contributions have been made for some years to allow users to exchange formal proofs between different provers. The main propositions consist in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a common formalism in which proofs can be translated and combined. To relate the independently developed mathematical libraries used in proof assistants, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems called MathTransfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.

mercredi 25 octobre 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Cédric Ho-Thanh, Chaitanya Leena-Subramaniam, Isaac Konan (Algebra and calculus, proofs and programs teams / Combinatorics team) · New PhD student introduction session

This special session will introduce three new PhD students who will each be giving a short talk.

vendredi 27 octobre 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Eric Finster () · The Generalized Blakers-Massey Theorem

vendredi 27 octobre 2017 · 14h30 · Salle 3058

Automates · Mikhail V. Volkov (Ural Federal University, Russie) · TBA