### Institut de Recherche en Informatique Fondamentale

** Research Institute for Foundations of Computer Science **

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

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

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

#### Events

Mardi 27 juin 2017 · Olympe-de-Gouges salle 255

Soutenance de thèse · Amina Doumane · On the infinitary proof theory of logics with fixed points