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:4833@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230622T110000
DTEND;TZID=Europe/Paris:20230622T123000
DTSTAMP:20260107T155955Z
URL:https://www.i2m.univ-amu.fr/evenements/simply-typed-%ce%b2-convertibil
 ity-is-tower-complete-even-for-safe-%ce%bb-terms/
SUMMARY:Lê Thành Dũng (Tito) Nguyễn (ENS Lyon): Simply typed β-conver
 tibility is TOWER-complete even for safe λ-terms
DESCRIPTION:Lê Thành Dũng (Tito) Nguyễn: We consider the following dec
 ision problem: given two simply typed λ-terms\, are they β-convertible? 
 Equivalently\, do they have the same normal form? It is famously non-eleme
 ntary\, but the precise complexity - namely TOWER-complete - is lesser kno
 wn. The talk will start by explaining what this means.\n\nOur original con
 tribution is to show that the problem stays TOWER-complete when the two in
 put terms belong to Blum and Ong's safe λ-calculus\, a fragment of the si
 mply typed λ-calculus arising from the study of higher-order recursion sc
 hemes. Previously\, the best known lower bound for this safe β-convertibi
 lity problem was PSPACE-hardness. Our proof proceeds by reduction from the
  star-free expression equivalence problem\, taking inspiration from the au
 thor's work with Pradic on "implicit automata in typed λ-calculi".
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