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:8193@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20150115T140000
DTEND;TZID=Europe/Paris:20150115T160000
DTSTAMP:20241210T143437Z
URL:https://www.i2m.univ-amu.fr/evenements/types-in-ludics/
SUMMARY:Eugenia Sironi (I2M\, Aix-Marseille Université): Types in Ludics
DESCRIPTION:Eugenia Sironi: This thesis proposes a representation of the no
 tion of type\, with a particular interest on dependent types\, in Ludics.\
 nLudics is a theory introduced by Girard. It comes from a fine analysis of
  the multiplicative\, additive fragment of polarized Linear Logic (MALL_p)
 . One of its aim is to reconstruct logic from the notion of interaction.\n
 A type is a class of objects that behave in the same way with respect to o
 ther objects.\nThe notion of type is common to several domains as Computat
 ion Theory\, Game Semantics and Martin-Lof's Intuitionistic Type Theory.\n
 Using the terminology of Martin-Lof\, the canonical terms of a type are th
 e primitive elements of the type\, that is the objects that characterize i
 t. The non-canonical terms are the terms obtained by applying some operati
 ons on canonical terms and that once computed give a canonical term. Terms
  are seen as programs and two terms are equal when their computation gives
  the same result\, that is the same canonical term.\nWe introduce the noti
 on of principal behaviour\, that is well-suited to represent canonical ter
 ms. We introduce also the notion of separable behaviour\, that gives us a 
 tool to define functions in a simple way.\nWe represent natural numbers\, 
 lists\, records\, dependent functions\, pairs and discuss dependent record
  types.\nWe focus then on Martin-Lof's Type Theory and propose the first s
 teps to represent some basic types and constructions.\n\n*Membres du jury 
 :\n-\n- Vito Michele Abrusci.\n- Claudia Faggian (PPS\, Paris 7).\n- Chris
 tophe Fouquéré (LIPN\, Paris 13)\, codirecteur.\n- Myriam Quatrini (I2M\
 , Marseille)\, codirectrice.\n- Laurent Regnier (I2M\, Marseille).\n- Chri
 stian Retoré (LIRMM\, Montpellier)\, rapporteur.\n\nLiens :\n- https://ca
 .linkedin.com/in/eugenia-sironi-7341a6b8/fr?trk=people-guest_people_search
 -card\n- theses.fr
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 015/01/Eugenia_Sironi.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:20141026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR