BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.3.3//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:9050@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20260521T110000
DTEND;TZID=Europe/Paris:20260521T123000
DTSTAMP:20260519T142035Z
URL:https://www.i2m.univ-amu.fr/evenements/minimum-and-maximum-lambda-term
 s/
SUMMARY:Adrienne Lancelot (Università di Bologna): Minimum and Maximum lam
 bda-Terms
DESCRIPTION:Adrienne Lancelot: The study of program preorders leads to more
  structure than that of program\nequivalences. Is it actually interesting 
 in the case of the uneffectful\nlambda-calculus? I will explain why order 
 properties are relevant\, as they may\nreformulate cornerstone results\, s
 uch as the genericity lemma. The genericity\nlemma\, indeed\, states the e
 xistence of minimum lambda-terms for a contextual\npreorder. One can duali
 ze this lemma to a co-genericity principle\, discussing\nmaximum terms. Ma
 ximum terms may feel intriguing\, but in a distributed setting\nthey repre
 sent a happy client\, which can no longer be used by a context in any\noth
 er way than being happy.\n\nI will discuss contextual preorders\, generici
 ty and co-genericity principles\,\nin both call-by-name and call-by-value.
  The application of these principles\nleads to a proof of the naturality o
 f contextual equivalence (or its preorder\nvariant) by giving sufficient c
 onditions for it to be maximal amongst\n(in)equational theories. The resul
 ts about call-by-name are formalized in the\nAbella proof assistant.\nThe 
 end of the talk will hopefully mention open questions and future work on\n
 the topic.\n\nBased on: Light Genericity FoSSaCS 2024\n[https://link.sprin
 ger.com/chapter/10.1007/978-3-031-57231-9_2]\, Barendregt's\nTheory of the
  lambda-calculus\, Refreshed and Formalized ITP 2025\n[https://doi.org/10.
 4230/LIPIcs.ITP.2025.13] and my PhD thesis 2025\n[https://theses.hal.scien
 ce/tel-05407883]
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20260329T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR