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.


Événements


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


mercredi 18 octobre 2017 · 14h30 · Salle 3052

Analyse et conception de systèmes · Nicolas Behr (IRIF) · The stochastic mechanics of graph rewriting via the rule algebra framework - an introduction

Reporting on joint work with V. Danos and I. Garnier, I will present a novel formulation of graph rewriting that permits to phrase the concept in a fashion akin to statistical physics. The key ingredient of this approach is the rule algebra framework, in which rewriting rules are interpreted as a type of diagrams endowed with a notion of sequential compositions. The focus of this talk will be the stochastic mechanics applications: once an associative algebra of rewriting rules is available in the form of the rule algebras, the full theory of continuous time Markov chains is at ones disposal. A number of explicit examples for computing in this formalism will be presented.


jeudi 19 octobre 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Martin Hyland (DPMMS, University of Cambridge) · Understanding Computation in Game Semantics


vendredi 20 octobre 2017 · 14h30 · Salle 3058

Automates · Sylvain Perifel (IRIF) · tba

tba


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 · Tba () · Séance nouveaux doctorants