16 novembre 2017, 11:00 : Séminaire

Maxime Lucas (I2M, Aix-Marseille), (à préciser)

9 novembre 2017

Séminaire Chocola à Lyon.

Du 23 au 25 octobre 2017

Réunion plénière du GDRI de logique linéaire et conférence à l’occasion du 70ème anniversaire de Jean-Yves Girard, à Rome.

19 octobre 2017, 11:00 : Séminaire

Laura Fontanella (I2M, Aix-Marseille), (à préciser)

12 octobre 2017

Séminaire Chocola à Lyon.

5 octobre 2017

Journée des nouveaux entrants de l’I2M

28 septembre 2017, 11:00 : Séminaire

Patrick Dehornoy (LMNO, Caen), La théorie des ensembles cinquante ans après Cohen

On présentera quelques résultats de théorie des ensembles récents, avec un accent sur l'hypothèse du continu et la possibilité de résoudre la question après les résultats négatifs bien connus de Gödel et Cohen, et sur les tables de Laver, qui sont des structures finies explicites, dont certaines propriétés combinatoires simples n'ont été établies jusqu'à présent que grâce à des axiomes de grand cardinal (non démontrables), une situation très paradoxale.

21 septembre 2017, 11:00 : Séminaire

Charles Grellois (LSIS, Aix-Marseille), Two Type-Theoretic Approaches to Probabilistic Termination

A fundamental result in lambda-calculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simply-typed lambda-calculus can be enriched with a recursion operator and, in this case, terms admitting a sized type always terminate. In this talk, we study a simply-typed lambda-calculus enhanced with a recursion operator and a probabilistic choice operator, and we focus on the probabilistic counterpart of termination: almost-sure termination (AST), that is, termination with probability 1. I will explain how the sized types approach can be extended to the probabilistic setting, so that we obtain a type system in which typability guarantees AST. I will then sketch ongoing work on a more powerful approach using dependent types, in order to capture AST for a wider class of programs. This is joint work with Dal Lago.

29 juin 2017

Séminaire Chocola à Lyon.

22 juin 2017, 10:30 : Séminaire

Victor Chepoi (LIF, AMU), Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières

On présente un contre-exemple à la conjecture de Thiagarajan (1996 et 2002) affirmant que les structures d'évènements régulières correspondent exactement à celles obtenues comme dépliages des réseaux de Petri 1-safe finis. Les structures d'évènements, les automates de trace sont des modèles fondamentaux pour la théorie de la concurrence. Il existe des interprétations élégantes de ces structures comme des objets combinatoires et géométriques, et on peut reformuler la conjecture dans ce cadre. Plus précisément, les domaines des structures d'évènements correspondent exactement aux graphes médians pointés et aux complexes cubiques CAT(0) pointés. Une condition nécessaire pour que la conjecture de Thiagarajan soit vérifiée est que les domaines des structures d'évènements régulières admettent un joli étiquetage régulier (regular nice labelling). Pour réfuter cette conjecture, on décrit le domaine d'une structure d'évènement régulière qui n'admet pas de tel étiquetage. Notre contre-exemple est basé sur une construction de Wise (1996 et 2007) d'un complexe de carrés de courbure non-positive dont le revêtement universel est un complexe de carrés CAT(0) contenant un plan muni d'un pavage apériodique. Travail en commun avec J. Chalopin.

15 juin 2017, 11:00 : Séminaire

Luc Pellissier (LIPN, Paris 13), Linear approximations, fibrations, intersection types

We investigate intersection types from the “type systems as functors” viewpoint, as recently given by Melliès and Zeilberger. After recasting type-theoretic notions such as subject reduction and subject expansion in functorial terms, we will give an intersection type system for linear logic (deriving from the fact that propositional linear logic is aproximated by its multiplicative fragment). Pulling back this intersection type system along translations of embeddings of a term language into linear logic gives a corresponding intersection type system. We discuss several instances of this general construction, recovering known systems and their usual properties.

Joint work with Damiano Mazza and Pierre Vial.

30 mai 2017 : Séminaire

Autour de l’hypothèse homotopique de Grothendieck

11:00: Edoardo Lanari (Macquarie University), Globular models for weak higher dimensional structures

The state of the art of higher category theory offers a wide variety of models for ∞-categories, and introduces the problem of comparing them. The two most important differences consist of the basic shapes we allow for our theory and their being algebraic or not. We will introduce a globular model for ∞- groupoids, that was first conjectured by A. Grothendieck, and describe its prominent features, If time permits, we will also outline how a comparison with topological spaces can be made quite explicitely, leading to the formulation of the so-called "Homotopy Hypothesis".

14:00: Simon Henry (Collège de France), Théorie homotopique des types et modèles algébriques pour les infinis catégories et groupoïdes

Dans son manuscrit “À la poursuite des champs” Grothendieck propose une définition “d'infini-groupoïde” ainsi qu'une notion d'équivalence entre eux et conjecture que la catégorie homotopique est équivalente à sa catégorie des infini-groupoïdes “à équivalence près”.

Cette conjecture (l'hypothèse d'homotopie) est toujours un problème ouvert, et il y a de très nombreuses questions basiques concernant cette notion d'infini-groupoïdes qui restent sans réponse. Pour cette raison, on préfère généralement utiliser les ensembles simpliciaux et les complexes de Kan pour définir la notion d'infini-groupoïde et servir de point de départ pour la théorie des catégories supérieures.

Cela dit l'apparition de la théorie homotopique des types nous donne de nouvelles motivations pour s'intéresser à cette notion d'infini-groupoïdes : tout d'abord n'importe quel type en théorie homotopique des types porte une structure d'infini-groupoïde au sens Grothendieck, ensuite, si la théorie des types est censée être la logique interne de certaines infini-catégories, il s'agit à priori d'infini-catégories globulaires, i.e. d'un genre plus proche de la définition de Grothendieck que des versions simpliciales. Enfin, on sait internaliser en théorie des types la définition d'infini-groupoïdes de Grothendieck, alors qu'on est très loin de savoir faire de même pour les approches simpliciales.

Dans cet exposé je vais présenter une nouvelle famille de définitions de la notion d'infini-groupoïde qui sont inspirées à la fois de celle de Grothendieck et de la théorie homotopique des types. Elles conservent certaines des bonnes propriétés de la définition de Grothendieck, mais échappent aux problèmes de celle-ci. On sait en particulier prouver l'analogue de l'hypothèse d'homotopie pour cette définition.

On énoncera aussi une conjecture technique précise, d'apparence simple, qui impliquerait que la définition de Grothendieck est un cas particulier de la nôtre, et qui donc impliquerait aussi l'hypothèse d'homotopie et résoudrait une partie des problèmes ouverts concernant la définition de Grothendieck.

11 mai 2017

Séminaire Chocola à Lyon.

4 mai 2017, 11:00 : Séminaire

Cyrille Chenavier (IRIF, Paris 7), Opérateurs de réduction et complétion de systèmes de réécriture linéaires

En réécriture, la confluence est une propriété garantissant que lorsque deux réductions sont issues d'un même terme, celles-ci confluent vers un terme commun. Dans cet exposé, on s'intéresse à la propriété de confluence de systèmes de réécriture linéaires décrits par des opérateurs de réduction. Cette description permet d'interpréter en termes de treillis les obstructions à la confluence. On en déduit des formulations de la confluence et de la complétion, ainsi qu'une méthode de complétion des systèmes de réécriture linéaires en termes de treillis.

13 avril 2017

Séminaire Chocola à Lyon.

30 mars 2017, 11:00 : Séminaire

Tom Hirschowitz (LAMA, USMB/CNRS), Shapely monads and analytic functors

In this work, we give precise mathematical form to the idea of a structure whose data and axioms are faithfully represented by a graphical calculus; some prominent examples are operads, polycategories, properads, and PROPs. Building on the established presentation of such structures as algebras for monads on presheaf categories, we describe a characteristic property of the associated monads — the shapeliness of the title — which says that ‘any two operations of the same shape agree’. In fact, shapeliness also gives a way to define the data and axioms of a structure directly from its graphical calculus, by generating a free shapely monad on the basic operations of the calculus.

This is joint work with Richard Garner.

23 mars 2017, 11:00 : Séminaire

Pierre Vial (IRIF, Paris 7), The Complete Unsoundness of Coinductive Intersection Types (and how to escape it)

Certain type assignment systems are known to guarantee or characterize normalization. The grammar of the types they feature is usually inductive. It is easy to see that, when types are coinductively generated, we obtain unsound type systems (meaning here that they are able to type some mute terms). Even more, for most of those systems, it is not difficult to find an argument proving that every term is typable (complete unsoundness). However, this argument does not hold for relevant intersection type systems (ITS), that are more restrictive because they forbid weakening. Thus, the question remains: are relevant ITS featuring coinductive types – despite being unsound – still able to characterize some bigger class of terms? We show that it is actually not the case: every term is typable in a standard relevant coinductive ITS that we call D. Moreover, we prove that semantical information can be extracted from the typing derivations of D, as the order of the typed terms. Our work also implicitly provides a new non sensible relational model for pure λ-calculus.

The proofs cannot be handled directly with usual intersection operators, so we introduce a new system that infinite sequences as intersection types (System S). System S provides nice combinatorial features that allows us to express the notion of typability of a term.

Eventually, we explain how soundness may be retrieved by means of a validity criterion that we call approximability. We then give an type-theoretical characterization of some class of infinitarily normalizing terms i.e. the set of terms whose Böhm tree does not hold bottom (the so called Hereditary Head Normalizing terms).

21 mars 2017, 10:30 : Séminaire

Gérard Berry (Collège de France), Logique intuitionniste et stabilisation dans les circuits électroniques

Attention: l’exposé a lieu en amphi Herbrand, 1er étage du site sud de l’I2M.

16 mars 2017, 11:00 : Séminaire

Domenico Ruoppolo (LIPN, Paris 13), Relational Graph Models and Observational theories

On présente les modèles de graphes relationnels (rgm), une sous-classe des modèles relationnels du lambda-calcul pur (les objects réflexifs dans la catégorie cartésienne fermée MRel engendrée par la sémantique relationnelle de LL). Les rgm sont une version relationnelle à la fois des modèles de graphes et des modèles filtres.

Nous nous servons des rgm pour obtenir la full abstraction (adéquation complète) par rapport à deux différentes théories observationnelles: celle qui considère les formes normales de tête comme termes observables (connu sous le nom de théorie H*) et celle qui prend les formes beta-normales comme observables (théories de Morris). Non seulement nous trouvons des modèles fully abstract, mais nous donnons une solution exhaustive au problème, en caractérisant tout rgm ayant la théorie H* ou la théorie de Morris. Les deux théories sont caractérisées par deux notions duales, données en termes de types intersection non-idempotents.

(joint work with Flavien Breuvart, Giulio Manzonetto and Andrew Polonsky)

9 mars 2017

Séminaire Chocola à Lyon.

2 mars 2017, 11:00 : Séminaire

Anupam Das (LIP (ÉNS Lyon), équipe PLUME), Monotonicity in Logic and Complexity

Monotonicity is a fundamental notion in mathematics and computation. For usual real-valued functions R → R this simply corresponds to the notion that a function is increasing (or decreasing) in its argument, however this can be parametrised by any partially ordered domain and codomain we wish. In computation we deal with programs that compute Boolean functions, {0,1} → {0,1}. Restricting to increasing functions over this structure can be seen as prohibiting the use of negation in a program; for instance monotone Boolean functions are computed by Boolean circuits without NOT gates. The idea of restricting negation scales to other models of computation, and for some important classes of functions the formulation is naturally robust, not depending on the particular model at hand, e.g. for the polynomial-time functions. Monotone computational problems abound in practice, e.g. sorting a string and detecting cliques in graphs, and 'nonuniform' monotone models of computation, such as monotone circuits, have been fundamental objects of study in computational complexity for decades.

In this talk I will propose a project that develops logical characterisations of monotone complexity classes, via a proof theoretic approach. Namely, the project will identify theories of arithmetic whose formally representable functions coincide with certain monotone classes, and also develop fundamental recursion-theoretic programming languages in which to extract the monotone functions themselves. In particular the project focusses on the role of structural proof theory, i.e. the duplication and erasure of formulae, in controlling monotonicity.

16 février 2017, 11:00 : Séminaire

Rodolphe Lepigre (LAMA, USMB), Proofs of programs and subtyping in PML2

PML2 is an ML style programming language that has the peculiarity of embedding an equational theory over its own programs, into its type system. This enables the specification of program properties as types, and they are then proved by constructing (terminating) programs inhabiting these types. After introducing the concepts of PML2, its type system and its classical realisability model, I will discuss recent work on subtyping and the implementation of PML2.

9 février 2017

Séminaire Chocola à Lyon.

2 février 2017, 11:00 : Séminaire

Claudia Faggian (IRIF, Paris 7), The Geometry of Parallelism: Probabilistic and Quantum Effects

(Joint work with Ugo Dal Lago, Benoit Valiron, Akira Yoshimizu)

What become the notions of confluence and convergence when a parallel rewrite system has both a probabilistic choice and the possibility of non-termination? We present a notion of Probabilistic Abstract Rewrite System (PARS) which deals with this issue by recovering a form of “diamond property”.

This result (the focus of the talk) is of interest in its own, but it is also key to introduce a Geometry of Interaction model for higher-order computation which has the ability to model commutative effects in a parallel setting, and to capture in particular quantum and probabilistic effects. The model (also sketched in the talk) comes with a multi-token machine, a proof net system, and a PCF-style language, which are all instances of PARS with a diamond property.

Being based on a rewrite system equipped with a memory, our model has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages. A success of our approach is to give (essentially for free) an adequate model for a fully-fledged quantum programming language in which entanglement, duplication, and recursion are all available.

26 janvier 2017, 11:00 : Séminaire

Gabriel Scherer (Programming Research Laboratory), Deciding simply-typed equivalence with sums and the empty type

The simply-typed λ-calculus, with only function types, is strongly normalizing, and its program equivalence relation is decidable: unlike in more advanced type system with polymorphism or effects, the natural "syntactic" equivalence (βη-equivalence) corresponds to natural "semantic" equivalence (observational or contextual equivalence), and is decidable. Adding product types (pairs) is easy and preserves these properties, but sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that Neil Ghani proved that the equivalence in presence of sums is decidable, and the situation in presence of the empty type (zero-ary sum) was unknown.

We propose an equivalence algorithm for sums and the empty type that takes inspiration from a proof-theoretic technique, named "focusing",designed for proof search. The exposition will be introductory; I will present the difficulties caused by sums and the empty type, present some of the existing approaches for sums in the literature, introduce focusing, and give a high-level intuition of our saturation-based algorithm and its termination argument.