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:8830@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20250925T110000
DTEND;TZID=Europe/Paris:20250925T123000
DTSTAMP:20250919T070224Z
URL:https://www.i2m.univ-amu.fr/evenements/linearization-via-rewriting/
SUMMARY:Federico Olimpieri (LIS\, Aix-Marseille): Linearization via Rewriti
 ng
DESCRIPTION:Federico Olimpieri: We introduce the structural resource λ-cal
 culus\, a new formalism inwhich strongly normalizing terms of the λ-calcu
 lus can naturally berepresented\, and at the same time any type derivation
  can be rewrittento its linearization. The calculus is shown to be normali
 zing andconfluent. Noticeably\, every strongly normalizable λ-term can be
 represented by a type derivation. This is the first example of a systemwhe
 re the linearization process takes place internally\, while remainingpurel
 y finitary and rewrite-based. We conclude by showing how ourlinearization 
 procedure bridges semantic and syntactic approaches toprogram approximatio
 n\, yielding new proof techniques and insights.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:Luminy - LIS\, salle 04.05\, Campus de Luminy\, Marseille\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Campus de Luminy\, Marseill
 e\, France;X-APPLE-RADIUS=100;X-TITLE=Luminy - LIS\, salle 04.05:geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20250330T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR