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:5803@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230112T110000
DTEND;TZID=Europe/Paris:20230112T123000
DTSTAMP:20241120T200221Z
URL:https://www.i2m.univ-amu.fr/evenements/an-interpretation-by-parametric
 ity-of-e-ha%cf%89-inside-ha%cf%89/
SUMMARY:Félix Castro (IRIF\, Paris Cité): An interpretation (by parame
 tricity) of E-HA^ω inside HA^ω
DESCRIPTION:Félix Castro: HA^ω (Higher Type Arithmetic) is a first
  order many sorted theory.\nIt is a conservative extension of HA (Heyt
 ing Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtai
 ned by extending the syntax of terms to all the System T : the objects of 
 interest here are the functionals of "higher types".\nWhile equality betwe
 en natural numbers is well understood (it is canonical and decidable)\, ho
 w equality between functionals can be defined ? From this question\, diffe
 rent versions of HA^ω arise: an extensional version (E-HA^ω) and an inte
 ntional version (I-HA^ω).\nIn this talk\, we will see how the study of a 
 (family of) partial equivalence relation(s indexed by the sorts of System 
 T) leads us to design a translation (by parametricity) from E-HA^ω (HA^ω
  + extensional equality at all level) to HA^ω (where equality is only def
 ined on natural numbers).\n[su_spacer size="10"]slides
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 022/12/image-ldp-logo-x150.jpg
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:STANDARD
DTSTART:20221030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR