An interpretation (by parametricity) of E-HA^ω inside HA^ω
Félix Castro
IRIF, Paris Cité
https://www.theses.fr/s230455
Date(s) : 12/01/2023 iCal
11h00 - 12h30
HA^ω (Higher Type Arithmetic) is a first order many sorted theory.
It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to all the System T : the objects of interest here are the functionals of “higher types”.
While equality between natural numbers is well understood (it is canonical and decidable), how equality between functionals can be defined ? From this question, different versions of HA^ω arise: an extensional version (E-HA^ω) and an intentional version (I-HA^ω).
In 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 defined on natural numbers).
[su_spacer size=”10″]slides
Emplacement
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)
Catégories
