Institut de Recherche en Informatique Fondamentale

Research Institute for Foundations of Computer Science

IRIF Université Paris 7 CNRS IRIF is a research laboratory co-founded by the CNRS and the University Paris-Diderot, resulting from the merging of the two research units LIAFA and PPS on January 1st, 2016.

The scientific objectives of the laboratory are at the core of computer science, focusing on: the mathematical foundations of computer science; computational models and proofs; models, algorithms and system design.

Upcoming seminars

Mercredi 28 juin 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Tommaso Petrucciani (PPS team) · Semantic subtyping: an introduction

Many type systems for programming languages include a notion of subtyping. Subtyping is often defined syntactically by a formal system, but this gets increasingly complex when union, intersection, and negation types are introduced.

In the semantic subtyping approach, instead, types are interpreted as sets and subtyping is defined in terms of set containment. Then, an algorithm is derived from the definition. While the algorithm is complex, the interpretation of types serves as a fairly simple specification. This approach also ensures that union and intersection on types behave as the corresponding operations on sets.

I will give an introduction to this approach and show how to define subtyping semantically for types including arrows, union, intersection, and negation, following [Frisch et al., 2008]. Then, we will look at ongoing work on adapting this approach (originally studied for call-by-value languages) to lazy semantics.

[Frisch et al., 2008] A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, JACM, 2008.

Mercredi 28 juin 2017 · 14h00 · Salle 3052

Vérification · Giuliano Losa (UCLA) · Paxos Made EPR — Decidable Reasoning about Distributed Consensus

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve higher-order concepts such as set cardinalities, arithmetic, and complex quantification.

This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Sch\“onfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos and Flexible Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos and Fast Paxos.

This is joint work with O. Padon, M. Sagiv, and S. Shoham.

Jeudi 29 juin 2017 · 11h00 · Salle 1007

Combinatoire énumérative et analytique · Wolfgang Steiner (IRIF) · Développements en base réelle et permutations

Elizalde (2011) a caractérisé les permutations qu'on obtient en ordonnant des éléments consécutifs dans une trajectoire d'une $\beta$-transformation, avec une base $\beta$ positive. Le cas d'une base $\beta$ entière correspond au full shift sur $\beta$ lettres, qui a été étudié par Amigó, Elizalde et Kennel (2008). Nous considérons les bases négatives. Travail en commun avec Émilie Charlier.

Vendredi 30 juin 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Andrew Polonsky · Lambda Calculus is a Groupoid

We discuss the problem of equality in type theory. We present an approach to defining higher equality structures in type theory. As an application, we study the lambda calculus from the multi-dimensional point of view. Taking equality between lambda terms (1-cells) to be beta conversion modulo permutation of redexes, we discover that the induced higher structure is a homotopy 1-type. That is, whenever there exists a higher cell between two β-conversions, the space of such cells is contractible. The key property of the lambda calculus responsible for this is Lévy’s projection calculus (AKA calculus of residuals). We conclude that the result holds for any theory which admits a presentation with such a calculus. For example, all (weakly) orthogonal TRSs describe homotopy 1-types.

Vendredi 30 juin 2017 · 16h30 · Salle 3052

Sémantique · Niccolò Veltri (Laboratory of Software Science, Tallinn) · Partiality and container monads

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this talk, we unveil the relation between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.


Lundi 10 - Jeudi 13 juillet 2017 · Amphi Turing

Clôture du projet MealyM