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:4807@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230601T110000
DTEND;TZID=Europe/Paris:20230601T123000
DTSTAMP:20260107T160651Z
URL:https://www.i2m.univ-amu.fr/evenements/profinite-lambda-terms-and-para
 metricity/
SUMMARY:Vincent Moreau (IRIF): Profinite lambda-terms and parametricity
DESCRIPTION:Vincent Moreau: This talk will present a definition of profinit
 e lambda-terms of\nany simple type. Profinite structures naturally appear 
 in automata theory\nas a way to speak about limiting behavior of finite wo
 rds\, giving rise to\nthe notion of profinite word. At the same time\, the
  Church encoding\nestablishes a one-to-one correspondence between finite w
 ords and\nsimply-typed lambda-terms\, taken modulo beta and eta\, of a typ
 e given by\ntheir finite alphabet. Our definition extends this corresponde
 nce between\nprofinite lambda-terms of a Church type and profinite words o
 ver the\nassociated alphabet. We start by introducing the set of profinite
 \nlambda-terms as a projective limit of finite sets of usual lambda-terms\
 ,\nconsidered modulo a notion of equivalence based on the finite standard\
 nmodel. We show that this resulting notion of profinite lambda-term\, comi
 ng\nfrom Stone duality\, lives in perfect harmony with the principles of\n
 Reynolds parametricity. Indeed\, we prove a parametricity theorem for Chur
 ch\nencodings of words\, stating that every parametric family of elements 
 in the\nfinite standard model is the interpretation of a profinite lambda-
 term.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - Ancienne BU\, Salle Séminaire2 (RdC)\, 163 Avenue de
  Luminy\, 13009 Marseille\, France\, 
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, 1300
 9 Marseille\, France\, ;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - Ancienne B
 U\, Salle Séminaire2 (RdC):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20230326T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR