Les séminaires sont communs avec l'équipe Plume (ENS Lyon) et ont lieu en salle de séminaire, premier étage du bâtiment Le Chablais, sur le site du Bourget du Lac ou à l'ENS Lyon.

Prochain séminaire :

Jeudi 22 novembre 2018 à 10h Léo Stefanesco (IRIF, Paris),
An Asynchronous Soundness Theorem for Concurrent Separation Logic

Résumé : (Masquer les résumés)
An Asynchronous Soundness Theorem for Concurrent Separation Logic. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. We develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems ⟦C⟧S and ⟦C⟧L which describe the operational behavior of the Code when confronted to its Environment (or Frame) – both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning and asynchronous strategy ⟦π⟧Sep with respect to both asynchronous semantics ⟦C⟧S and ⟦C⟧L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ:⟦C⟧S→⟦C⟧L, from the stateful semantics ⟦C⟧S to the stateless semantics ⟦C⟧L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races. This is joint work with Paul-André Melliès. Organization of the talk: In a first part, I will give a high level view of our semantics and of the soundness theorem, essentially as it appeared in our previous paper. In a second part, I will talk in more details about our new semantics of CSL, which has a more algebraic flavor (work in progress).

Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date décroissante. Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2019, toutes ensemble.

Année 2018

Jeudi 25 janvier 2018 à 10h Youssef Fares (Amiens),
Autour de la conjecture de Poonen sur les polynômes quadratiques

Résumé : (Masquer les résumés)
Soit c un nombre rationnel. Considérons le polynôme φ(X) = X^2 - c. On s’intéressse aux cycles de φ dans Q. Plus précisément, on s’intéresse à l’une des conjectures de Poonen selon laquelle tout cycle de φ dans Q admet une longueur au plus égale à 3. Dans notre exposé, on discutera de cette conjecture et on rappellera les résultats connus. En suite, on utilisera des moyens arithmetiques, combinatoriaux et analytiques simples pour étudier des cas particuliers de ce problème. Les outils utilisés dans cet exposé sont accessibles aux étudiants de master 2.

Jeudi 01 février 2018 à 10h Thomas Rubiano (LIPN, Paris 13),
Implicit Computational Complexity meets Compilers

Résumé : (Masquer les résumés)
Complexity theory helps us predict and control resources, usually time and space, consumed by programs. Static analysis on specific syntactic criterion allows us to categorize some programs. A common approach is to observe the program’s data’s behavior. For instance, the detection of non-size-increasing programs is based on a simple principle : counting memory allocation and deallocation, particularly in loops. This way, we can detect programs which compute within a constant amount of space. This method can easily be expressed as property on control flow graphs. Because analyses on data's behaviour are syntactic, they can be done at compile time. Because they are only static, those analyses are not always computable or easily computable and approximations need are needed. ``Size-Change Principle'' from C. S. Lee, N. D. Jones et A. M. Ben-Amram presented a method to predict termination by observing resources evolution and a lot of research came from this theory. Until now, these implicit complexity theories were essentially applied on more or less toy languages. This thesis applies implicit computational complexity methods into ``real life'' programs by manipulating intermediate representation languages in compilers. This give an accurate idea of the actual expressivity of these analyses and show that implicit computational complexity and compilers communities can fuel each other fruitfully. As we show in this thesis, the methods developed are quite generals and open the way to several new applications.

Jeudi 08 février 2018 à 10h, Lyon Séminaire Chocola (ENS Lyon),
TBA

Résumé : (Masquer les résumés)
TBA

Mercredi 28 février 2018 à 10h Eric Goles (Engineering Faculty of the Adolfo Ibanez University, Santiago, Chile),
Dynamics and Complexity of Majority Automata: application to some discrete social models

Résumé : (Masquer les résumés)
A Majority Automata consists of applying over the vertices of a undirected graph (with states 0’s and 1’s) an operator that chooses the most represented state among the neighbors of a vertex. This rule is applied in parallel over all the nodes of the graph. When the graph is a regular lattice ( in one or more dimensions) it is called the Majority Cellular Automata. In this seminar we will study the computational complexity of the following prediction problem: PRED: Given an initial configuration and a specific site initially at state a ( 0 or 1), is there a time step T≥1 such that this site changes state? The complexity of PRED is characterized by the possibility to find an algorithm that give the answer faster than the running of the automata simulation in a serial computer. More precisely, if we are able to determine an algorithm running in a parallel computer in polylog time (class NC). Otherwise, the problem may be P-Complete ( one of the most dificult in class P of Polynomial problems) or … worse. We will applied this kind of results to the discrete Schelling’s segregation model. Also we will present the Sakoda’s Social Discret model.

Jeudi 08 mars 2018 à 10h Étienne Miquey (Nantes),
The algebraic structure of classical realizability models.

Résumé : (Masquer les résumés)
Implicative algebras, developed by Alexandre Miquel, are very simple algebraic structures generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such a way that they allow to express in a same setting the theory of forcing (in the sense of Cohen) and the theory of classical realizability (in the sense of Krivine). Besides, they have the nice feature of providing a common framework for the interpretation both of types and programs. The main default of these structures is that they are deeply oriented towards the λ-calculus, and that they only allows to faithfully interpret languages in call-by-name. To remediate the situation, we introduce two variants of implicative algebras: disjunctive algebras, centered on the “par” (⅋) connective of linear logic (but in a non-linear framework) and naturally adapted to languages in call-by-name; and conjunctives algebras, centered on the “tensor” (⊗) connective of linear logic and adapted to languages in call-by-value. Amongst other properties, we will see that disjunctive algebras are particular cases of implicative algebras and that conjunctive algebras can be obtained from disjunctive algebras (by reversing the underlying order).

Jeudi 15 mars 2018 à 10h, Lyon Séminaire Chocola (ENS Lyon),
TBA

Mercredi 21 mars 2018 à 10h, B-4A-CANTONS-63 Buket Eren (Galatasaray University, Istambul, Turquie.),
Autour de l'équation de Markov

Résumé : (Masquer les résumés)
Les nombres de Markov sont des entiers positifs qui apparaissent dans les triplets de solutions de l’équation diophantienne, x^2+y^2+z^2 = 3xyz, appelée l’équation de Markov. Il est possible de trouver tous les solutions à partir d’un triplet par un algorithme simple. Pourtant, il y a un célèbre problème ouvert formulé par Frobenius : est-il vrai qu'étant donné un entier positif z, il existe au plus un couple (x,y) d’entiers positifs avec x < y < z tel que (x,y,z) soit une solution? Ces nombres apparaissent dans le contexte des fractions continues et de l’approximation diophantienne des nombres réels irrationnels par des nombres rationnels. Ils apparaissent aussi dans de très nombreux domaines des mathématiques comme les formes quadratiques binaires, la géométrie hyperbolique et la combinatoire des mots etc... Le but de cette exposé est de présenter une partie de la théorie de Markov qui est construite autour de l’équation de Markov et de donner la conjecture d’unicité sur les nombres de Markov. Au final, on introduira une involution des irrationnels susceptible d’être pertinente pour le sujet.

Jeudi 22 mars 2018 à 10h, B-3-POLE MONTAGNE-030 Oleg Karpenkov (Department of Mathematical Sciences, University of Liverpool),
Global relations for toric singularities

Résumé : (Masquer les résumés)
In this talk we will discuss a link between geometry of continued fractions and global relations for singularities of complex projective toric surfaces. The results are based on recent development of lattice trigonometric functions that are invariant with respect to Aff(2,Z)-group action.

Jeudi 29 mars 2018 à 09h Maxime Lucas (Nantes),
Réécriture de dimension supérieur et catégories cubiques

Résumé : (Masquer les résumés)
La réécriture de dimension supérieure a pour origine des travaux de Squier sur le problème du mot dans les monoïdes. A partir d'une présentation d'un monoïde, Squier a pu calculer en basse dimension des invariants homotopiques de ce monoïde. Depuis, elle a été adaptée à d'autres structures, et en particulier aux PRO, où elle permet de prouver des théorèmes de cohérence comme celui de MacLane pour les catégories monoïdales. Par ailleurs, dans le cas des monoïdes, les constructions de réécriture ont été étendues en dimension supérieure. Au cours de cet exposé, je montrerai comment il est possible d'unifier ces théories de réécriture dans diverses structures. En particulier, ceci permet de réinterpréter les constructions effectuées en réécriture en termes homotopiques. Cette réinterprétation s'appuie en particulier sur la notion de omega-catégorie cubique et sur le produit de Gray.

Jeudi 12 avril 2018 à 10h, Lyon Séminaire Chocola (ENS Lyon),
TBA

Jeudi 19 avril 2018 à 10h Arpita Korwar (Université Paris 7),
Computational complexity of polynomial factorization - a survey

Résumé : (Masquer les résumés)
The ring of multivariate polynomials F[x_1, x_2, ..., x_n] is a unique factorization domain. We consider the following problem: ``Is there an 'efficient' algorithm that outputs a non-trivial factor of the given input polynomial''. This question has applications in algebraic complexity, for example, in proving the connection between polynomial identity testing (PIT) and lower bounds. In this talk, we will consider the closure of various classes of polynomial families under factorization. [Kaltofen86-90] studied this problem for VP. A slew of work in the recent years has brought it back into the limelight: [DSY09] studied circuits of small depth and factors of a special form, [Oliveria16] studied formulas of small depth, [DSS18] studied ABPs and formulas, [CKS18] studied the polynomial class VNP. We will take a look at these algorithms and state some open problems in the area.

Jeudi 17 mai 2018 à 10h, Lyon Séminaire Chocola (ENS Lyon),
TBA

Jeudi 24 mai 2018 à 10h Tom Hirschowitz (LAMA Chambéry),
Familial monads and structural operational semantics

Résumé : (Masquer les résumés)
Structural operational semantics is a family of syntactic formats for specifying the operational semantics of programming languages, in the form of a labelled transition system. Fiore and his collaborators have proposed an abstract framework for structural operational semantics based on bialgebras, in which they managed to prove that bisimilarity is a congruence. However, their framework does not scale well to languages with variable binding. We give an abstract account of structural operational semantics based on Weber's parametric right adjoint monads, which encompasses variable binding. On the example of pi-calculus, the key idea is that, while Fiore models the syntax through a monad on a certain presheaf category, we use a subtly different presheaf category inspired by our previous work on sheaf models for concurrent languages. The crucial consequence is that the relevant monad is a parametric right adjoint. This yields a very simple proof of congruence of bisimilarity.

Jeudi 31 mai 2018 à 14h Pierre Cagne (Institut de Recherche en Informatique Fondamentale (Équipe PPS - Paris Diderot)),
Bifibrations de Quillen, quand la dépendence rencontre l'homotopie

Résumé : (Masquer les résumés)
Je commencerai par une introduction basique aux différents outils utilisés dans mon domaine de recherche, à savoir la théorie des catégories, l'algèbre homotopique à la Quillen et l'interprétation de la logique à la Lawvere. Aucune connaissance n'est prérequise et je m'appuierai sur des analogies algébriques accessibles à tous mathématiciens (monoides, groupes, etc.) et sur des exemples pertinents en regard des thématiques du LIMD. Une fois ces notions introduites, je présenterai le résultat central de travaux récents effectués avec Paul-André Melliès : étant donnée une bifibration E-->B où la base et les fibres sont équipées de structures de catégories de modèles, quelles sont les conditions pour recoller ces dernières en une structure de catégorie de modèles sur la catégorie totale E ? J'essaierai enfin d'expliquer les motivations de ces travaux qui trouvent leur origine à la fois dans la théorie de l'homotopie catégorique et dans la sémantique de la théorie des types dépendents.

Jeudi 14 juin 2018 à 10h Henning Basold (ENS Lyon),
Breaking the Loop: Recursive Proofs for Coinductive Predicates

Résumé : (Masquer les résumés)
In this talk, I present a framework for recursive proofs of coinductive predicates, which are defined via functor liftings to fibrations. This framework is based on the so-called later modality and Löb-induction. Intuitively, the role of the later modality is thereby to control the use of coinduction hypotheses. Since the framework works on certain fibrations, it can be instantiated in very diverse situation like, for instance, set-based predicates and relations, quantitative predicates and relations, syntactic first-order logic, or dependent type theory. Apart from showing the underlying technical constructions of the framework, I will demonstrate how it can be used in those examples. Moreover, I will briefly talk about some recent progress, in collaboration with Katya Komendantskaya and Yue Li, in the direction of automatic proof search for this framework.

Jeudi 21 juin 2018 à 10h Luc Pellissier (LIPN),
Entropy and Complexity Lower Bounds

Résumé : (Masquer les résumés)
Finding lower bounds in complexity theory has proven to be an extremely difficult task. We analyze three proofs of lower bounds that use heavy techniques from algebraic geometry through the lense of dynamical systems. Interpreting programs as graphings – generalizations of dynamical systems that model Girard's Geometry of Interaction, we show that the three proofs share the same structure and use algebraic geometry to give a bound on the topological entropy of the system representing the program. This work, joint with Thomas Seiller, aims at proposing Geometry of Interaction derived methods to study dynamical properties of models of computation beyond Curry-Howard.

Jeudi 08 novembre 2018 à 10h Paolo Pistone (Wilhelm Schickard Institut, Eberhard Karls Universität Tübingen),
Relating realizability and parametricity semantics of System F

Résumé : (Masquer les résumés)
Realizability and parametricity are two well-known approaches to the semantics of System F, the architectural language for polymorphism. Many well-known realizability semantics can be recast in a simple topological form as induced by closure operators over sets of lambda-terms. This allows to generalize some completeness results known in the literature to a wide class of semantics (including Krivine's saturated sets and several variants of Girard's reducibility candidates), and to relate realizability with parametricity and dinaturality, an approach to parametricity arising from the functorial semantics of polymorphism. Our main result is that for a general class of realizability semantics (those which satisfy a particular topological property) one can prove a ``parametricity theorem'' stating that closed realizers are parametric and a ``dinaturality theorem'' stating that closed realizers of positive types are dinatural. We compare our results with Wadler's approach which sees realizability and parametricity as some sort of adjoint functors. Finally, we briefly discuss the case of Girard's original definition of reducibility candidates, whose ``not trivial and somehow mysterious'' [Riba 2007] structure does not fit yet within our approach.

Jeudi 22 novembre 2018 à 10h Léo Stefanesco (IRIF, Paris),
An Asynchronous Soundness Theorem for Concurrent Separation Logic

Résumé : (Masquer les résumés)
An Asynchronous Soundness Theorem for Concurrent Separation Logic. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. We develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems ⟦C⟧S and ⟦C⟧L which describe the operational behavior of the Code when confronted to its Environment (or Frame) – both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning and asynchronous strategy ⟦π⟧Sep with respect to both asynchronous semantics ⟦C⟧S and ⟦C⟧L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ:⟦C⟧S→⟦C⟧L, from the stateful semantics ⟦C⟧S to the stateless semantics ⟦C⟧L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races. This is joint work with Paul-André Melliès. Organization of the talk: In a first part, I will give a high level view of our semantics and of the soundness theorem, essentially as it appeared in our previous paper. In a second part, I will talk in more details about our new semantics of CSL, which has a more algebraic flavor (work in progress).

Jeudi 29 novembre 2018 à 10h Adrien Guatto (IRIF, Paris),
Towards A General Guarded Lambda-Calculus

Résumé : (Masquer les résumés)
Guarded recursion has emerged as a natural paradigm for programming with infinite data structures in type theory and high-assurance functional languages. In the first part of this talk, I will present some intuitions behind guarded recursion, using programming examples. In a second part, I will discuss ongoing work on a typed lambda-calculus equipped with rich facilities for defining and manipulating guarded recursive types.

Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date décroissante. Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2019, toutes ensemble.