13 décembre 2018

Séminaire Chocola à Lyon.

6 décembre 2018, 11:00 : Séminaire

Victor Chepoi (LIS, Aix-Marseille), Matroides et leur graphes des bases

En première partie de l'exposé nous présentons une introduction aux matroïdes et leur définition axiomatique : libres, bases, circuits, fonction de rang, fermeture, dualité, algo glouton.

Dans une deuxième partie, nous considérons le graphe des bases d'un matroïde, le complexe des triangles et des carrés de ce graphe, ainsi que le polyèdre des bases d'un matroïde.

Nous présentons une caractérisation locale-vers-globale des graphes de bases: il s'agit exactement des graphes dont le complexe des triangles et carrés est simplement connexe et chaque boule de rayon 3 est isomorphe à une boule d'un graphe de base.

Ce dernier résultat est un travail en commun avec J. Chalopin et D. Osajda, J. Combin. Th. Ser. B 114 (2015).

29 novembre 2018, 11:00 : Séminaire

Luc Pellissier (Universidad de la República, Montevideo, Uruguay), Linear Implicative Algebras, towards a BHK interpretation of linear logic

Implicative Algebras were recently introduced as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly.

In this ongoing work with Alexandre Miquel, we show how linear logic fits in this picture.

22 novembre 2018, 11:00 : Séminaire

Zeinab Galal (IRIF, Paris 7), Connecting Models of Differential Linear Logic with Reloids

Species of structures were introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics. Species are connected to Girard's normal functor semantics of λ-calculus where terms are interpreted as power series with sets as coefficients. Fiore et al. presented a generalised definition that both encompasses Joyal's species and constitutes a model of differential linear logic. For generalised species of structures, types are interpreted as groupoids which provides the connection with combinatorics whereas they are interpeted as sets in Girard's normal functors and in the relational model. To investigate how these models interact, we introduce a variant of the relational model where objects are setoids (sets equipped with an equivalence relation) and morphisms are relations. We obtain a new model of differential linear logic (named Reloids) that allows for a less degenerate collapse from species than the one to normal functors or relations. We then show how to construct functors preserving the linear logic structure between these four models.

15 novembre 2018

Séminaire Chocola à Paris.

11 octobre 2018, 11:00 : Séminaire

Thomas Ehrhard (IRIF, Paris 7), Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types

On montrera comment interpréter μLL - la logique linéaire propositionnelle avec plus petits (μ) et plus grands (ν) points fixes de types - dans les espaces cohérents, puis dans les espaces cohérents avec totalité. Le premier modèle ne fait pas la différence entre μ et ν, alors que le second, bâti sur le premier, interprète μ et ν de façons différentes. La même technique s'adapte à beaucoup d'autres modèles, et notamment aux espaces de finitude. μLL peut être vu comme un langage de programmation fortement normalisant contenant le système T de Gödel et permettant de définir de nombreux "types de données" (listes, arbres, mais aussi streams etc).

Travail en collaboration avec Farzad Jafrrahmani.

4 octobre 2018, 11:00 : Séminaire

Giulio Manzonetto (LIPN, Paris 13), Revisiting Call-by-value Bohm trees in light of their Taylor expansion

The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. We show that such an extension allows to define a satisfying notion of Bohm(-like) tree and a theory of program approximation in the call-by-value setting. We prove that all lambda terms having the same Bohm tree are observationally equivalent, and characterize those Bohm-like trees arising as actual Bohm trees of lambda terms.

We also compare this approach with Ehrhard's theory of program approximation based on the Taylor expansion of lambda terms, translating each lambda term into a possibly infinite set of so-called resource terms. We provide sufficient and necessary conditions for a set of resource terms in order to be the Taylor expansion of a lambda term. Finally, we show that the normal form of the Taylor expansion of a lambda term can be computed by performing a normalized Taylor expansion of its Bohm tree. From this it follows that two lambda terms have the same Bohm tree if and only if the normal forms of their Taylor expansions coincide.

Joint work with Emma Kerinec and Michele Pagani.

13 septembre 2018, 11:00 : Séminaire

Lê Thành Dũng Nguyễn (LIPN, Paris 13), Évaluation sémantique en logique linéaire élémentaire

Après avoir passé en revue l'utilisation des techniques d'évaluation sémantique pour caractériser des classes de complexité en lambda-calcul simplement typé (en particulier les travaux de Hillebrand et Kanellakis), nous décrirons un nouveau résultat s'appliquant à une logique du second ordre : les langages décidés par des programmes en logique linéaire élémentaire (ELL) opérant sur des chaînes de Church et de type de sortie !!Bool sont exactement les langages rationnels. (En ajoutant des types récursifs, on obtient tout le temps polynomial, ce qu'a montré Baillot.) La preuve repose principalement sur l'existence d'une sémantique finie de la logique linéaire multiplicative du second ordre, obtenue par quotient observationnel. Ce premier résultat pourrait ouvrir la voie à une étude fine de la complexité dans les logiques allégées, tenant compte du contrôle exercé conjointement par les propriétés géométriques de la syntaxe et le typage, ce dernier étant reflété dans la sémantique. Ainsi, nous formulerons une caractérisation conjecturale de l'espace logarithmique dans ELL.

Travail réalisé avec Thomas Seiller.

6 septembre 2018, 11:00 : Séminaire

Étienne Miquey (Gallinette, Inria-LS2N, Nantes), The algebraic structure of classical realizability models

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).

5 juillet 2018, 11:00 : Séminaire

Valentin Blot (LRI, Paris Sud), Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

14 juin 2018, 11:00 : Séminaire

Pierre Clairambault (LIP, ÉNS Lyon), The true concurrency of Herbrand's theorem

Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers.

In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.

This is joint work with Aurore Alcolei, Martin Hyland, and Glynn Winskel.

Du 12 au 13 juin 2018

Rencontre de réalisabilité au CIRM, organisée par Laura Fontanella et Guillaume Geoffroy.

Voir le site de la rencontre.

7 juin 2018, 11:00 : Séminaire

Pierre Vial (Gallinette, Inria-LS2N, Nantes), Representing permutations without permutations, or the expressive power of sequence types

An intersection type system with given features (strict or not, idempotent or not, relevant or not, rigid or not...) characterizing, e.g., a notion of normalization can be presented in various ways. Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on, e.g., typing derivations. We previously introduced system S, featuring a sequential intersection: a sequence is a family of types indexed by a set of integers. However, one may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one with permutations. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S (sequential intersection) has full expressive power over multiset/ permutation-inclusive intersection. We do so in the most general setting, i.e. by considering coinductive type grammars, so that this work also applies in the study of the infinitary relational model.

26 avril 2018, 11:00 : Séminaire

Andrea Gagna (I2M, Aix-Marseille), Les petites catégories comme modèles des types d'homotopie (suite)

La théorie de l'homotopie des petites catégories a été introduite par Grothendieck avec la définition du foncteur nerf, qui permet de donner une notion sensible d'équivalence faible parmi les petites catégories. Dans sa thèse, Illusie montre (et il attribue la preuve à Quillen) que la catégorie de l'homotopie des petites catégories est équivalente aux types d'homotopie. On donnera une variante de cette preuve qui utilise le théorème A de Quillen.

19 avril 2018, 11:00 : Séminaire

Alexis Saurin (IRIF, Paris 7), Logical by-need

L'analyse de l'appel par nécessité (aussi appelé évaluation paresseuse) est complexe, d'autant plus lorsqu'on considère des opérateurs de contrôle. Ceci suggère de faire appel à la logique, par nécessité, plutôt qu'à chercher à trouver une solution fondée sur de pures considérations opérationnelles. Dans ce séminaire, je présenterai deux telles approches du logical by-need: le premier inspiré par le système L de Curien et Herbelin et le second de la réduction linéaire de tête de Danos et Regnier.

La première approche ne sera qu'évoquée: l'exposé visera surtout à construire un calcul paresseux à partir de la réduction linéaire de tête en trois étapes, à le comparer aux calculs de la littérature et à montrer que cette construction s'étend naturellement aux opérateurs de contrôle fournissant un λμ-calcul paresseux. Selon le temps restant, je discuterai de variantes de l'appel par nécessité (notamment la pleine paresse). Cet exposé s'appuie sur des travaux conduits avec Pédrot ainsi qu'Ariola, Downen, Herbelin et Nakata.

5 avril 2018, 11:00 : Séminaire

Amina Doumane (LIP, ÉNS Lyon), Completeness for identity-free Kleene Lattices

We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. This equational theory was previously proved to coincide with that of language models and to be ExpSpace- complete; expressions of the corresponding syntax moreover make it possible to denote precisely those languages of graphs that can be accepted by Petri automata. Finite axiomatisability was missing to obtain the same picture as for Kleene algebra, regular expressions, and (word) automata.

Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.

29 mars 2018, 11:00 : Séminaire

Eduard Balzin (CMLS, École Polytechnique), Les familles de catégories en géométrie et algèbre

Dans cet exposé on parlera des problèmes mathématiques qui peuvent être étudiés en utilisant le formalisme des familles de catégories. Beaucoup d’exemples de familles proviennent de la géométrie, où on considère divers champs à valeurs dans les catégories, et on prend les catégories des sections sous-jacentes. Un autre contexte est celui de l'algèbre, où on peut étudier les familles associées aux catégories monoïdales M. La catégorie des sections d’une telle famille contient les objets algèbres dans M.

Étant donné une famille des catégories munies d'équivalences faibles, on peut se demander si la catégorie des sections est un bon invariant au sens « infini-catégorique ». Nous expliquerons ce problème en détail, en répondant positivement à une conjecture de Hirschowitz et Simpson pour les familles provenant de champs de catégories. Si le temps le permet, on esquissera une approche à cette question dans le cadre des catégories monoïdales.

L'exposé ne supposera aucune connaissance de théorie de l'homotopie, seul une familiarité avec le langage des catégories est requise.

8 mars 2018, 11:00 : Séminaire

Andrea Gagna (I2M, Aix-Marseille), Les petites catégories comme modèles des types d'homotopie

La théorie de l'homotopie des petites catégories a été introduite par Grothendieck avec la définition du foncteur nerf, qui permet de donner une notion sensible d'équivalence faible parmi les petites catégories. Dans sa thèse, Illusie montre (et il attribue la preuve à Quillen) que la catégorie de l'homotopie des petites catégories est équivalente aux types d'homotopie. On donnera une variante de cette preuve qui utilise le théorème A de Quillen.

22 février 2018, 11:00 : Séminaire

Assia Mahboubi (LS2N, Nantes & Inria), Une preuve assistée par ordinateur de l'irrationalité de zeta(3)

L'étude des valeurs de la fonction zeta de Riemann aux entiers impairs est encore aujourd'hui un sujet de recherche actif en théorie des nombres. R. Apéry a obtenu en 1978 un succès spectaculaire en établissant l'irrationalité de zeta(3). Mais le statut, rationnel ou irrationnel des autres entiers positifs impairs est encore inconnu à ce jour. Le point crucial de la présentation originale d'Apéry réside dans l'observation que deux suites particulières sont solutions d'une même récurrence, remarque qui permet d'estimer leurs comportements asymptotiques respectifs. Cette récurrence miraculeuse était difficile à deviner, mais elle s'est aussi révélé difficile à vérifier pour l'auditoire d'Apéry. Depuis les années 90, des chercheurs en combinatoire et en calcul formel ont conçu des algorithmes efficaces qui permettent de "deviner" de telles récurrences, et ainsi de faire des preuves "par calcul formel". Dans cet exposé nous présentons et discutons une preuve formelle de l'irrationalité de zeta(3) basée sur une session de calcul formel qui exécute de tels algorithmes.

(en collaboration avec Frédéric Chyzak, Thomas Sibut-Pinote et Enrico Tassi)

15 février 2018, 11:00 : Séminaire

Giulio Manzonetto (LIPN, Paris 13), Refutation of Sallé's Longstanding Conjecture

The lambda-calculus possesses a strong notion of extensionality, called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. We will first show that Morris's theory satisfies the omega-rule. We will then demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhm trees.

18 janvier 2018, 11:00 : Séminaire

Hadrien Batmalle (IRIF, Paris 7), Préservation de propriétés du modèle de départ en réalisabilité classique

La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines... axiomatisés au moyen d'algèbres de réalisabilité). Elle produit ainsi des modèles de ces théories, et se révèle être une généralisation du forcing de Cohen. Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ "raisonnable", supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera des modèles de réalisabilité classique issus d'algèbres de réalisabilité usuelles, mais construits sur des modèles de départ "non-triviaux", et on utilisera un nouveau résultat de Krivine pour exporter certaines propriétés du modèle de départ au modèle de réalisabilité.