Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil > Séminaires > Séminaires et Groupes de travail hebdomadaires > Logique et Interactions

Séminaire Logique et Interactions

par Lozingot Eric, Vaux Lionel - publié le , mis à jour le

Agenda

Séminaire

  • Jeudi 28 février 11:00-12:30 - Claudia FAGGIAN - IRIF, Paris 7

    Lambda Calculus and Probabilistic Computation

    Résumé : In order to model higher-order probabilistic computation, a natural approach is to take the lambda calculus as a paradigm, and to enrich it with an operator which models probabilistic choice. The resulting calculus is however not confluent ; such an issue is typically handled in the literature by fixing a deterministic reduction strategy.
    Following [Plotkin75], we wish to preserve the key distinction between a calculus and a programming language. The former defines terms and reduction rules, and satisfy confluence, the latter is specified by a deterministic strategy (an abstract machine). Standardization is what relates the two : the programming language implements the standard strategy associated to the calculus. We propose two probabilistic lambda calculi, based respectively on the call-by-value and call-by-name parameter passing mechanism. The common root of the two calculi is a further calculus based on Linear Logic, which allows us to develop a unified, modular approach.
    (joint work with Simona Ronchi Della Rocca)

    JPEG - 13.7 ko
    Claudia FAGGIAN

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 7 mars 11:00-12:30 - Lionel VAUX AUCLAIR - I2M, Aix-Marseille Université

    Combinatoire de l’élimination des coupures de MLL, et une application au développement de Taylor de MELL

    Résumé : TBA

    JPEG - 10 ko
    Lionel VAUX

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 21 mars 11:00-12:30 - Luigi SANTOCANALE - LIS, Aix-Marseille Université

    Quantales MIX *-autonomes et l’ordre faible continu

    Résumé : L’ensemble des permutations sur une ensemble fini possède la structure de treillis connue comme l’ordre faible de Bruhat. Cette structure s’étend aux mots sur un alphabet fini Σ = x, y, z, . . . tels que chaque lettre a un nombre fixé d’occurrences. Ces treillis sont connus comme "treillis multinomiaux" et, quand card(Σ) = 2, comme "treillis de chemins dans le réseau" (lattices of lattice path). Si on interprète les lettres x, y, z, . . . comme des axes, ces mots peuvent se voir comme des chemins discrets sur une grille dans un cube de dimension d = card(Σ).
    -
    Dans cet exposé j’expliquerai comment étendre cet ordre aux (images des) chemins continus croissants de l’intervalle [0,1] vers le cube [0,1]^d (qui préservent les extrémités 0 et 1). On obtient ainsi un treillis noté L_d([0,1]) ; l’outil clé de cette construction est le quantal (ou treillis résidué involutif) L_∨([0,1]) des fonctions sup-continues (cad, croissantes continue à gauche) de l’intervalle [0,1] vers lui même. Il s’agit d’un quantal (treillis résidué) cyclique *-autonome (involutif), qui satisfait la règle MIX.
    -
    Nous exposerons la structure des treillis L_d([0,1]) : ils sont auto-duaux, engendrés par sups par les éléments sup-irréductibles, il ne possèdent pas des éléments complétement sup-irréductibles. Quand d = 2, L_d([0,1]) = L_∨([0,1]) est la complétion de Dedekind-MacNeille des chemins discrets avec sauts rationnels. Quand d ≥ 3, cette propriété n’est plus vraie, mais chaque élément de L_d([0,1]) est un sup d’infs des chemins avec sauts rationnels.

    JPEG - 12.1 ko
    Luigi SANTOCANALE

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 28 mars 11:00-12:30 - Thomas STREICHER - TU Darmstadt

    Simplicial into cubical

    Résumé : TBA

    JPEG - 8.9 ko
    Thomas STREICHER

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 25 avril 11:00-12:30 - Raphaëlle CRUBILLÉ - IRIF, Paris 7

    Probabilistic stable functions on discrete cones are power series

    Résumé : The category of probabilistic coherence spaces (PCoh_ !), introduced by Danos and Ehrhard, is a fully abstract model for PCF with *discrete* probabilities, where morphisms can be seen as power series. The category Cstab_m, of measurable cones and measurable stable functions, has been introduced by Ehrhard, Pagani and Tasson as a model for PCF with *continuous* probabilities.
    In this talk, we will study the shape of stable functions when they are between discretecones : we will show that they can actually be seen as generalized power series. The proof is based on a generalization of a theorem from real analysis due to Bernstein, that states that all absolutely monotonous functions on reals are power series. From there, we will build a full and faithful functor from PCoh_ ! into Cstab_m that moreover preserves the cartesian closed structure.

    JPEG - 22.1 ko
    Raphaëlle CRUBILLÉ

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 2 mai 11:00-12:30 - Marie KERJEAN - Gallinette, INRIA-LS2N, Nantes

    Polarized models of Differential Linear Logic

    Résumé : TBA

    JPEG - 3.9 ko
    Marie KERJEAN

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 23 mai 11:00-12:30 - Aurore ALCOLEI - LIP, ÉNS Lyon & Computer Laboratory, Cambridge

    Concurrent Games with side-information

    Résumé : Game semantics is an interactive denotational semantics : a denotation specifies the behaviour of a term/proof with respect to its environment. As such it is one of the most intensional model available in the Curry-Howard community.
    Despite their intensional persprective, game models still omit a number of computational informations by hiding away internal reductions. This power of abstraction is at the core of the methodology of denotational semantics in that it aims to provide invariants under reduction. Yet, in some cases, this abstraction is too strong and prevents to capture some desirable informations.
    In this talk, I will present how the model of concurrent game and strategies on event structures can be naturally extended with annotations from any (in)equational theory to keep track of side-information, that is information that may vary with interactions but does not influence their outcomes.
    Depending on time and audience’s interest, I will present this construction through two independent results : on the logic side I will show how this model instantiated with terms can be used to give a new interpretation and proof of the Herbrand’s theorem ; on the programming side I will introduce a semantics for R-IPA, a concurrent programming language with shared memory and an operational semantics keeping track of resource consumption, based on an instantiation of that same model with annotations being functions over reals.

    Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud - Bâtiment TPR2
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

groupe de travail

Manifestation scientifique

Descriptif
Nature Séminaire et Groupe de travail
Intitulé Logique et interactions
Responsable Lionel Vaux
Équipe de rattachement Logique de la Programmation (LDP) du Groupe Arithmétique Géométrie Logique et Représentations (AGLR, ex-LUM)
Fréquence 1 à 2 séances par mois
Jour-Horaire Jeudi. 11h-12h30
Lieu Luminy, salle des séminaires 304-306 (accès)
Lien http://iml.univ-mrs.fr/ldp/seminaire/

Contact : lionel.vaux_AT_univ-amu.fr