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

  • Lundi 10 février 2014 14:00-15:00 - Giuseppe Greco - Delft University of Technology

    Proof theory for dynamic logics

    Résumé : We introduce a multi-type display calculus for (intuitionistic) dynamic epistemic logic and (concurrent) propositional dynamic logic, which we refer to as Dynamic Calculi. The display approach is suitable to modularly chart the space of dynamic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculi with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems that enjoy a generalisation of the Curry-Belnap cut-elimination meta-theorem.



    Giuseppe Greco

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

    Exporter cet événement

  • Mardi 18 mars 2014 11:00-12:00 - Benedikt Ahrens - IRIT, Toulouse

    Category theory in the Univalent Foundations

    Résumé : The Univalent Foundations is an extension of Intensional Martin-Löf Type Theory (MLTT) recently proposed by V. Voevodsky. Its novelty is the Univalence Axiom which implements the idea that indistinguishable types should be equal by identifying equality of types with isomorphism of types. When formalizing category theory in traditional, set-theoretic foundations, a significant discrepancy between the foundational notion of "sameness" - equality - and its categorical notion arises : most category-theoretic concepts are invariant under weaker notions of sameness than equality, namely isomorphism in a category or equivalence of categories. We show that this discrepancy can be avoided when formalizing category theory in Univalent Foundations. In this talk I first give an introduction to Voevodsky’s Univalent Foundations. Afterwards I define categories and univalent categories within Univalent Foundations, and develop basic category theory. The two main results of our work are the following :

    1. Two univalent categories are equivalent (in the category-theoretic sense) if and only if they are equal (in the type-theoretic sense).
    2. Any category can be turned into a univalent category via a universal construction, which we call the Rezk completion.
    JPEG - 10.2 ko
    Benedikt Ahrens

    Lieu : Luminy, Amphithéâtre Herbrand 130-134 - Institut de Mathématiques de Marseille (UMR 7373)
    Site Sud
    Campus de Luminy, Case 907
    13288 MARSEILLE Cedex 9

    Exporter cet événement

  • Vendredi 28 mars 2014 14:00-15:00 - Benoît Valiron - PPS, Paris 7

    Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

    Résumé : In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is described, and several examples based on Church numerals are presented.

    JPEG - 11.4 ko
    Benoît VALIRON
    Benoît Valiron

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

    Exporter cet événement

  • Vendredi 18 avril 2014 11:00-12:00 - Marc Lasson - Cambridge

    Canonicity of groupoids laws using parametricity theory

    Résumé : The synthetic approach to weak ω-groupoids promoted by the univalent foundation program is the idea that (homotopy) type theory should be the primitive language in which spaces, points, paths, homotopies are derived. Following this approach, spaces are represented by types, points by inhabitants and paths by equalities between points (also known as identity types) and algebraic properties of these objects should not be unforced a priori (for instance by axioms) but should be derived directly from the language. Following this approach requires to be convinced that definitions of new operations should be canonical, in the sense that no important choice should be made by picking an implementation of these operations instead of an other. Identities, inversion and concatenation of path, associativities, idempotency of inversion, horizontal and vertical compositions of 2-paths, are all examples of groupoid laws.
    Parametricity has been introduced by Reynolds to study the polymorphic abstraction of system F. It refers to the concept that well-typed programs cannot inspect the type their arguments ; they must behave uniformly with respect to abstract types. Reynolds formalizes this notion by showing that polymorphic programs satisfy the so-called logical relations defined by induction on the structure of types. Dependent type systems are expressive enough to state their own parametricity theory.
    In this talk, we will focus on the consequences of this remark when applied to identity types and we will use it to prove that all implementations of a given groupoid law are provably equal to each other.

    JPEG - 13.5 ko
    Marc LASSON

    Lieu : Luminy, 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

  • Vendredi 18 avril 2014 14:00-15:00 - Philip Scott - University of Ottawa, Canada

    Coordinatizing MV algebras and AF C*-algebras by inverse monoids

    Résumé : TBA
    Joint work with M. Lawson.

    GIF - 10.2 ko
    Philip SCOTT

    Lieu : Luminy, 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

  • Vendredi 25 avril 2014 11:00-12:00 - Laurent Poinsot - Paris 13

    Sur le groupoïde de géométrie d’une variété équationnelle équilibrée

    Résumé : Patrick Dehornoy a construit un monoïde de fonctions partiellement définies sur une algèbre de termes sur un domaine d’opérateurs (signature) S, dit conoïde de géométrie, qu’il associe à toute variété équationnelle V de S-algèbres déterminée par une congruence équilibrée, i.e., pour laquelle deux termes équivalents possèdent les mêmes ensembles de variables. Dans cet exposé je dégagerai la nature profonde de cette construction qui est celle d’un groupoïde. Je montrerai que celui-ci n’est que l’image d’un groupoïde plus fondamental par une représentation fidèle (un fonceur fidèle dans le groupoïde des ensembles et bijections). Ce dernier gouverne alors la "géométrie" du calcul dans la variété V, au sens où son action sur un terme correspond à des réécritures (au sens de la réécriture de termes), et hérite de surcroît d’une structure fonctorielle de S-algèbre. Si le temps me le permet, j’aborderai la généralisation de cette construction obtenue en remplaçant l’algèbre des termes par une algèbre libre dans une variété équationnelle déterminée par une congruence "linéaire".

    JPEG - 9 ko
    Laurent POINSOT

    Lieu : Luminy, 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 12 juin 2014 14:00-15:00 - Clément Aubert - I2M, Marseille

    Programmation logique, unification et espace logarithmique

    Résumé : Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique.
    Un travail en collaboration avec Marc Bagnol, Paolo Pistone et Thomas Seiller.

    JPEG - 8.7 ko
    Clément AUBERT

    Lieu : Luminy, 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

  • Lundi 23 juin 2014 10:00-11:00 - François Métayer - PPS, Paris 7

    Les orientaux de Street revisités par Burroni

    Résumé : La construction d’un nerf des omega-catégories, c’est-à-dire un foncteur de la catégorie des omega-catégories vers celle des ensembles simpliciaux repose sur l’existence d’une famille adéquate de simplexes orientés, définis par Street. J’expliquerai comment l’approche de Burroni simplifie la construction de ces objets à la combinatoire délicate, en exploitant les propriétés d’un foncteur des cylindres sur omega-Cat.

    JPEG - 15.3 ko
    François MÉTAYER

    Lieu : Luminy, 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

  • Mercredi 9 juillet 2014 11:00-12:00 - Lionel Vaux - I2M, Marseille

    La forte normalisabilité des λ-termes

    Résumé : La forte normalisabilité des λ-termes est caractérisée, à travers leur développement de Taylor, par une structure de finitude sur l’ensemble des termes avec ressources (et ça marche même sans uniformité).

    JPEG - 10 ko
    Lionel VAUX

    Lieu : Luminy, 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 | 6 | 7 | 8 | 9 | ... | 14

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