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 2 février 2017 11:00-12:00 - Claudia FAGGIAN - IRIF, Paris 7

    The geometry of parallelism : probabilistic and quantum effects

    Résumé : 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.
    (Joint work with Ugo Dal Lago, Benoit Valiron, Akira Yoshimizu)
    Référence : https://arxiv.org/pdf/1610.09629v2.pdf

    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
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 16 février 2017 11:00-12:00 - Rodolphe LEPIGRE - LAMA, Université de Savoie

    Proofs of programs and subtyping in PML2

    Résumé : 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.

    JPEG - 13.2 ko
    Rodolphe LEPIGRE

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

    Exporter cet événement

  • Jeudi 2 mars 2017 11:00-12:00 - Anupam DAS - LIP (ÉNS Lyon), équipe PLUME

    Monotonicity in Logic and Complexity

    Résumé : 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.

    JPEG - 10.2 ko
    Anupam DAS

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

    Exporter cet événement

  • Jeudi 16 mars 2017 11:00-12:00 - Domenico RUOPPOLO - LIPN, Paris 13

    Relational graph models and observational theories

    Résumé : 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)

    JPEG - 6.9 ko
    Domenico RUOPPOLO

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

    Exporter cet événement

  • Mardi 21 mars 2017 11:00-12:00 - Gérard BERRY - Collège de France, Paris

    Logique intuitionniste et stabilisation dans les circuits électroniques

    Résumé : TBA

    Médaille d’or 2014 du CNRS
    JPEG - 6.7 ko
    Gérard BERRY

    Lieu : Amphi Herbrand (1er étage) - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Jeudi 23 mars 2017 11:00-12:00 - Pierre VIAL - IRIF, Paris 7

    The complete unsoundness of coinductive intersection types (and how to escape it)

    Résumé : 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).

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

    Exporter cet événement

  • Jeudi 30 mars 2017 11:00-12:00 - Tom HIRSCHOWITZ - LAMA, Université de Savoie

    Shapely monads and analytic functors

    Résumé : 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.

    JPEG - 11.2 ko
    Tom HIRSCHOWITZ

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

    Exporter cet événement

  • Jeudi 4 mai 2017 11:00-12:00 - Cyrille CHENAVIER - IRIF, Paris 7

    Opérateurs de réduction et complétion de systèmes de réécriture linéaires

    Résumé : 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.

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

    Exporter cet événement

  • Mardi 23 mai 2017 11:00-12:00 - Matteo ACCLAVIO - LMNO, Caen

    Syntaxe et sémantique des diagrammes de preuve

    Résumé : TBA

    JPEG - 6.8 ko
    Matteo ACCLAVIO

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

    Exporter cet événement

  • 1 | 2 | 3 | 4 | 5

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