An interpretation (by parametricity) of E-HA^ω inside HA^ω

Félix Castro
IRIF, Paris Cité

Date(s) : 12/01/2023   iCal
11 h 00 min - 12 h 30 min

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).


Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)


Retour en haut 

Secured By miniOrange