An Interpretation of E-HA^w inside HA^w

Félix Castro

Higher Type Arithmetic (HA^w) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of higher types. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HA^w arise, such as an extensional version (E-HA^w) and an intentional version (I-HA^w). In this work, we will see how the study of partial equivalence relations leads us to design a translation by parametricity from E-HA^w to HA^w.

In Alberto Ciaffaglione and Carlos Olarte: Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2023), Rome, Italy, 2nd July 2023, Electronic Proceedings in Theoretical Computer Science 396, pp. 52–66.
Published: 17th November 2023.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: