Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil >

4 juillet 2019: 2 événements

Séminaire

  • Séminaire Logique et Interactions

    Jeudi 4 juillet 11:00-12:30 - Pierre HYVERNAT - LAMA, Université Savoie Mont Blanc

    Checking correctness for recursive definitions with mixed inductive and coinductive types

    Résumé : The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. If the language is lazy, it also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda.
    Unfortunately, when inductive and coinductive types are nested, this is unsound : there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistent.
    Using ideas from L. Santocanale about circular proof and parity games, I’ll show how the SCP can be used to check "totality" of recursive definitions. Besides the SCP, the main ingredient is a more informative of notion call-graph, and I’ll sketch the proof of correctness by defining their "untyped" semantics using power domains.

    JPEG - 29.4 ko
    Pierre HYVERNAT

    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
    Document(s) associé(s) :

    En savoir plus : Séminaire Logique et Interactions

  • Séminaire Représentations des Groupes Réductifs (RGR)

    Jeudi 4 juillet 14:00-15:00 - Raphaël BEUZART-PLESSIS - I2M, CNRS, Marseille

    Une nouvelle preuve du lemme fondamental de Jacquet-Rallis

    Résumé : Le lemme fondamental de Jacquet-Rallis est une identité locale entre intégrales orbitales relatives qui apparaît naturellement dans une approche par la formule des traces relative à la conjecture de Gan-Gross-Prasad pour les groupes unitaires. Il a été démontré peu après sa formulation par Z.Yun en caractéristique positive par des méthodes similaires à celles développées par Ngô pour le lemme fondamental endoscopique et transférer en caractéristique nulle par J.Gordon via des techniques de théorie des modèles. Dans cet exposé, j’expliquerai une preuve alternative de ce lemme fondamental en caractéristique nulle qui est purement locale et basée sur des outils d’analyse harmonique.

    JPEG - 10.4 ko
    Raphaël BEUZART-PLESSIS

    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
    Document(s) associé(s) :

    En savoir plus : Séminaire Représentations des Groupes Réductifs (RGR)

4 juillet 2019: 1 événement

Manifestation scientifique

  • Agenda ERC IChaos

    Du 29 juin au 7 juillet - Alexander BUFETOV

    Summer School "Analysis, Geometry, and Pde" Nordfjordeid 2019

    Résumé : Invited speaker

    Lieu : Sophue Lie Center - Nordfjordeid, Norway

    Exporter cet événement

En savoir plus : Agenda ERC IChaos