BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7673@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20161214T140000
DTEND;TZID=Europe/Paris:20161214T153000
DTSTAMP:20241210T072728Z
URL:https://www.i2m.univ-amu.fr/evenements/reecriture-de-diagrammes-applic
 ations-a-la-theorie-des-categories-et-a-la-theorie-de-la-demonstration-mat
 teo-acclavio/
SUMMARY:Matteo Acclavio (I2M\, Aix-Marseille université): Réécriture de 
 diagrammes : applications à la théorie des catégories et à la théorie
  de la démonstration
DESCRIPTION:Matteo Acclavio: http://www.theses.fr/s165038\nDans le dernier 
 siècle\, nombreux sciences ont enrichi leur syntaxe pour pouvoir modeler 
 des interactions. Entre eux on peut compter l’informatique\, la physique
  quantique\, et aussi la biologie et l’économie : toutes ces sciences s
 ont des exemples de domaines qui ont besoin d’une syntaxe et d’une sé
 mantique soit pour la concurrence que pour la séquentialité.\nLes diagra
 mmes des cordes sont bien adaptés à cet effet. Dans leur syntaxe on peut
  retrouver deux compositions : une composition parallèle et une compositi
 on séquentielle\, qui peuvent interagir à travers une loi d’interchang
 e. Si on considère cette loi comme une égalité\, les diagrammes de cord
 es sont une syntaxe pour les catégories monoidales strictes\, avec une re
 présentation graphique plus intuitive que les formules algébriques tradi
 tionnelles.\nDans cette thèse\, on étudie cette syntaxe de dimension 2 e
 t sa sémantique. On considère la réécriture des diagrammes et on donne
  des applications de cette méthode :\n• une preuve détaillée du théo
 rème de cohérence de Mac Lane pour les catégories monoidales symétriqu
 es basée sur un système de réécriture convergent donnée en arXiv:1606
 .01722 \;\n• une interprétation des dérivations de preuves avec les di
 agrammes de preuve pour le fragment MELL de la logique linéaire\, qui cap
 ture l’équivalence de preuves. On peut vérifier la séquentialité en 
 temps linéaire\, c’est à dire vérifier si un diagramme corresponds à
  une preuve. Cette interprétation est une extension de celle pour le frag
 ment MLL donnée en arXiv:1606.09016 en donnant aussi un résultat de éli
 mination du coupure.\nAbstract : String diagram rewriting: applications in
  category and proof theory\nIn the last century\, several sciences enriche
 d their syntax in order to model interactions. Not only computer science a
 nd quantum physics\, but also biology and economics are examples of fields
  requiring syntax and semantics for concurrency as well as for sequentiali
 ty.Retour ligne automatique\nString diagrams are suitable for that purpose
 . In that syntax\, we have two compositions : the parallel one and the seq
 uential one\, which may interact by the interchange rule. If we consider t
 his rule as an equality\, string diagrams are a syntax for strict monoidal
  categories\, with a more intuitive graphical representation than traditio
 nal algebraic formulas.Retour ligne automatique\nIn this thesis\, we study
  this 2-dimensional syntax and its semantics. We consider diagram rewritin
 g and we give two applications of those methods :Retour ligne automatique\
 n• a detailed proof of Mac Lane’s coherence theorem for symmetric mono
 idal categories based on convergent diagram rewriting\, which is given in 
 arXiv:1606.01722 \;Retour ligne automatique\n• an interpretation of proo
 f derivations by string diagrams for the MELL fragment of linear logic\, w
 hich captures proof equivalence. We get a linear sequentializability test 
 to verify if a diagram corresponds to a proof . This interpretation extend
 s the one for the MLL fragment given in arXiv:1606.09016\, providing also 
 a cut-elimination result.\n-\nMembres du jury :\nDirecteur de thèse\n- Yv
 es LAFONT (I2M\, Marseille)\n-\nRapporteurs proposés :\n- Willem HEIJLTIE
 S (Lecturer &amp\; Prize fellow\, Bath)\n- Samuel MIMRAM (CR HDR\, Ecole P
 olytechnique)\n- Pierre-Louis CURIEN (DR\, INRIA Paris)\n-\nAutres membres
  du jury :\n- Michele ABRUSCI (Professore Ordinario\, Roma 3)\n- Myriam QU
 ATRINI (MCF HDR\, AMU\, I2M\, Marseille)\n- Luigi SANTOCANALE (PR\, AMU)\n
 - Lorenzo TORTORA de FALCO (Professore Associato\, Roma 3)\n-\n\nLiens :\n
 - theses.fr\n- SUDOC Abes
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Matteo_Acclavio.jpg
CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20161030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR