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.


Poste de maître de conférences


Un poste de maître de conférences est ouvert au concours 2017, affecté à l'IRIF, sur les thématiques de l'unité. Consulter la fiche de poste.


Prochains séminaires


Jeudi 23 février 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Marcelo Fiore (University of Cambridge) · An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures

The starting point of the talk will be the identification of structure common to tree-like combinatorial objects, exemplifying the situation with abstract syntax trees~(as used in formal languages) and with opetopes (as used in higher-dimensional algebra). The emerging mathematical structure will be then formalized in a categorical setting, unifying the algebraic aspects of the theory of abstract syntax of [2,3] and the theory of opetopes of [5]. This realization conceptually allows one to transport viewpoints between these, now bridged, mathematical theories and I will explore it here in the direction of higher-dimensional algebra, giving an algebraic combinatorial framework for a generalisation of the slice construction of [1] for generating opetopes. The technical work will involve setting up a microcosm principle for near-semirings and subsequently exploiting it in the cartesian closed bicategory of generalised species of structures of [4]. Connections to (cartesian and symmetric monoidal) equational theories, lambda calculus, and algebraic combinatorics will be mentioned in passing.

[1] J.Baez and J.Dolan. Higher-Dimensional Algebra III. n-Categories and the Algebra of Opetopes. Advances in Mathematics 135, pages 145-206, 1998.

[2] M.Fiore, G.Plotkin and D.Turi. Abstract syntax and variable binding. In 14th Logic in Computer Science Conf. (LICS'99), pages 193-202. IEEE, Computer Society Press, 1999.

[3] M.Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57–68. IEEE, Computer Society Press, 2008.

[4] M.Fiore, N.Gambino, M.Hyland, and G.Winskel. The cartesian closed bicategory of generalised species of structures. In J. London Math. Soc.}, 77:203-220, 2008.

[5] S.Szawiel and M.Zawadowski. The web monoid and opetopic sets. In arXiv:1011.2374 [math.CT], 2010.


Vendredi 24 février 2017 · 14h30 · Salle 3052

Automates · Daniela Petrisan (IRIF) · Quantifiers on languages and topological recognisers

In the first part of the talk I will recall the duality approach to language recognition. To start with, I will explain the following simple fact. The elements of the syntactic monoid of a regular language $L$ over a finite alphabet $A$ are in one to one correspondence with the atoms of the finite sub-Boolean algebra of $P(A^*)$ generated by the quotients of $L$. This correspondence can be seen as an instance of Stone duality for Boolean algebras, and has lead to a topological notion of recognition for non-regular languages, the so called Boolean spaces with internal monoids.

A fundamental tool in studying the connection between algebraic recognisers, say classes of monoids, and fragments of logics on words is the availability of constructions on monoids which mirror the action of quantifiers, such as block products or other kinds of semidirect products. In the second part of the talk I will discuss generalisations of these techniques beyond the case of regular languages and present a general recipe for obtaining constructions on the topological recognisers introduced above that correspond to operations on languages possibly specified by transducers.

This talk is based on joint work with Mai Gehrke and Luca Reggio.


Vendredi 24 février 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Cyrille Chenavier · Caractérisation et construction de bases de Gröbner par les opérateurs de réduction


Mardi 28 février 2017 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Laurent Viennot (INRIA - IRIF) · To be announced


Mardi 28 février 2017 · 11h00 · Salle 3052

Sémantique · Ran Chen 1) · Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm

There is a growing interest in programs proofs checked by computer. Proofs about programs are often very long and have to face a huge amount of cases due to the multiplicity of programs variables and the precise details of the programs. This is very frustrating since we would like to explain the proofs of correctness and publish them in scientific articles. However if one considers simple algorithms, we would expect to explain their proofs of correctness in the same way as we explain a mathematical proof for a non too complex theorem.

We present a human readable and rather intuitive formal proof for the classical Tarjan-1972 algorithms for finding strongly connected components in directed graphs. Tarjan’s algorithm consists in an efficient one-pass depth-first search traversal in graphs which traces the bases of strongly connected components. We describe the algorithm in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer.



Événements


1) Inria