Institut de Mathématiques de Luminy

SÉMINAIRES 2010
Logique et Interactions

Organisateurs :
Yves Lafont (tél. 04 91 26 96 37)
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.


Agathe Chollet

jeudi 16 décembre
Agathe Chollet
(LMI, La Rochelle) :

Formalismes non classiques pour le traitement informatique de la topologie et de la géométrie discrète


Page personnelle : http://agathechollet.ozazar.org/

Yves Lafont

jeudi 9 décembre
Yves Lafont et Pierre Rannou
(IML, Marseille) :

Diagrammes, Σ-diagrammes
et propriétés des co-opérations


Page personnelle : http://iml.univ-mrs.fr/~lafont/


jeudi 18 novembre
au CIRM
Pierre Gillibert
(Charles Univ., Prague) :

Points critiques entre variétés de treillis

Homepage: http://www.math.unicaen.fr/~giliberp/

Vito Michele Abrusci

jeudi 21 octobre
Michele Abrusci (Univ. Roma 3) :

à 10h30
Syllogismes et logique linéaire


à 14h
Espaces cohérents et ontologies formelles
(travail en cours avec Christophe Fouqueré et Marco Romano)

Homepage: http://host.uniroma3.it/dipartimenti/filosofia/Docenti/infoprof/Abrusci.html

jeudi 14 octobre
Reporté
Tom Hirschowitz (LAMA, Chambéry) :
Algebraic structures from shapes

Homepage: http://www.lama.univ-savoie.fr/~hirschowitz/

Abstract: An important part of categorical computer science, at least in proportion, consists of extracting the algebraic essence of computational structures. The mother of all examples of this is the correspondence between simply-typed λ-calculus and cartesian closed categories. Presenting such algebraic structures can be subtle, especially when seeking so-called coherence, which exhibits the equivalence of algebra with some combinatorial structure. The talk is an introduction by example to a technique for constructing algebraic structures from their expected combinatorial description, bypassing the tedious work of presentation. The pattern is as follows:
(1) the combinatorial description provides a monad which yields the expected structure,
(2) the Leinster-Weber theory of local right adjoint monads generates a presentation for it.


jeudi 30 septembre
Guillaume Munch-Maccagnoni (PPS, Paris 7) :
Une décomposition polarisée
des traductions CPS délimitées

Homepage: http://perso.ens-lyon.fr/guillaume.munch/

Résumé : La logique classique de Girard (LC) permet d'expliquer les traduction CPS (continuation-passing style) de la logique classique dans la logique intuitionniste à travers une décomposition en trois étapes:
1 - Le choix d'un ordre d'évaluation exprimé en termes de polarités classiques.
2 - La traduction d'un calcul polarisé avec opérateurs de contrôle (ici: LC) dans un cadre polarisé de nature plus intuitionniste (ici: LLP, dans lequel les notions de positif/négatif correspondent plus volontiers à celles de type de valeur et de type de calcul en informatique).
3 - La traduction de LLP vers le λ-calcul, qui permet de rendre compte d'artéfacts bureaucratiques propres aux traductions CPS: réductions administratives, aplatissement de la symétrie possible entre entrées et sortie.
Je donne une telle décomposition polarisée pour des traductions CPS issues de l'étude des opérateurs de contrôle délimité, qui permettent d'exprimer une classe d'effets plus grande que les opérateurs de contrôle de la logique classique.
L'enjeu est de montrer que la polarisation de LC, comme paradigme de calcul qui mélange termes stricts et paresseux, n'est pas limitée aux effets de la logique classique; et que par ailleurs des systèmes de «types avec effets» de la littérature peuvent se reconstruire à travers les décompositions polarisées usuelles de l'appel par nom ou par valeur.


Yael Fregier

vendred
i 2 juillet

Yaël Frégier (Luxembourg) :
Bases de Gröbner en théorie des opérades,
d'après Dotsenko et Khoroshkin

Homepage: http://wwwen.uni.lu/research/fstc/unite_de_recherche_en_mathematiques/people/yael_fregier

 


jeudi 4 mars
Thomas Seiller (IML) :
Graphes d'interaction

jeudi 25 février
Pierre Lofredi (étudiant MDFI) :
Machines à registres et machines affines

jeudi 4 février
Yves Lafont (IML) :
Problème du mot et géométrie de la réécriture
jeudi 28 janvier
Pierre Rannou (IML) :
Co-opérations et réécriture de diagrammes

mercredi 20 janvier
à 11h
Claudia Fagian (PPS, Paris 7) :
Ludics with repetitions:
exponentials, internal and full completeness



Jean-Louis_Loday

jeud
i 14 janvier

Jean-Louis Loday (IRMA, Strasbourg) :
Bigèbres généralisées

Page web : http://www-irma.u-strasbg.fr/~loday/

Résumé : Les bigèbres classiques ont une structure algébrique d'algèbre associative et une structure cogébrique de cogèbre associative. Ces deux structures sont en liaison via une relation de compatibilité (relation de Hopf). Il existe d'autres types de bigèbres obtenues en modifiant ces différentes structures. Pour certaines d'entre elles on sait généraliser les théorèmes classiques de Poincaré-Birkhoff-Witt et Cartier-Milnor-Moore.



Alejandro_Diaz-Caro

jeud
i 7 janvier

Alejandro Díaz-Caro (LIG, Grenoble) :
A system F accounting for scalars

(joint work with Pablo Arrighi)
Homepage: http://membres-liglab.imag.fr/diazcaro/

Abstract: The linear-algebraic λ-calculus extends the λ-calculus with the possibility of making arbitrary linear combinations of λ-calculus terms a.t+b.u. In this paper we provide a System F-like type system for the linear-algebraic λ-calculus, which keeps track of “the amount of a type” that is present in a term. We show that this scalar type system enjoys both the subject-reduction property and the strong-normalisation property, which constitute our main technical results. The latter yields a significant simplification of the linear-algebraic λ-calculus itself, by removing the need for some restrictions in its reduction rules — and thus leaving it more intuitive. More importantly we show that our type system can readily be modified into a probabilistic type system, which guarantees that terms define correct probabilistic functions. Thus we are able to specialize the linear-algebraic λ-calculus into a higher-order, “probabilistic” λ-calculus. Finally we discuss the more long-term aims of this reseach in terms of establishing connections with linear logic, and building up towards a quantum physical logic through the Curry-Howard isomorphism. Thus we begin to investigate the logic induced by the scalar type system, and prove a no-cloning theorem expressed solely in terms of the possible proof methods in this logic.

 

EL, le 16 décembre 2010