Félix Castro
IRIF, Paris Cité
https://www.theses.fr/s230455
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).
slides
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories