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:4760@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230504T110000
DTEND;TZID=Europe/Paris:20230504T123000
DTSTAMP:20260107T160334Z
URL:https://www.i2m.univ-amu.fr/evenements/quantitative-inhabitation-for-d
 ifferent-lambda-calculi-in-a-unifying-framework/
SUMMARY:Victor Arrial (IRIF): Quantitative inhabitation for different lambd
 a calculi in a unifying framework
DESCRIPTION:Victor Arrial: We study the inhabitation problem for a language
  called 𝜆!\, a subsuming paradigm (inspired by call-by-push-value) bein
 g able to encode Call-by-Name and Call-by-Value strategies of functional p
 rogramming. The type specification uses a non-idempotent intersection type
  system\, which is able to capture quantitative properties about the dynam
 ics of programs. Our general methodology can be used to derive inhabitatio
 n algorithms for CbN and CbV lambda-calculi.\nIn the presentation\, we det
 ail the tools and explain the method solving this inhabitation problem. We
  will in particular explore the notion of approximants and their behaviour
  through the CbN and CbV encodings\, the formers being at the core of the 
 completeness of the method. We will also give a general overview of the in
 habitation algorithm as well as a few insights on its termination.\nhttps:
 //www.irif.fr/~kesner/papers/popl23.pdf[su_spacer size="10"]
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